@ARTICLE{polynom9,
TITLE = {{P}rime Representing Polynomial with 10~Unknowns},
AUTHOR = {P\k{a}k, Karol},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
VOLUME = {30},
NUMBER = {{\bf 4}},
PAGES = {255--279},
YEAR = {2022},
DOI = {10.2478/forma-2022-0021}
}
@ARTICLE{hilb10_8,
TITLE = {{P}rime Representing Polynomial with 10~Unknowns -- {I}ntroduction. Part II},
AUTHOR = {P\k{a}k, Karol},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
VOLUME = {30},
NUMBER = {{\bf 4}},
PAGES = {245--253},
YEAR = {2022},
DOI = {10.2478/forma-2022-0020}
}
@ARTICLE{hilb10_7,
TITLE = {{P}rime Representing Polynomial with 10~Unknowns -- {I}ntroduction},
AUTHOR = {P\k{a}k, Karol},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
VOLUME = {30},
NUMBER = {{\bf 3}},
PAGES = {169--198},
YEAR = {2022},
DOI = {10.2478/forma-2022-0013}
}
@article{hilb10_6,
TITLE = {Prime {R}epresenting {P}olynomial},
AUTHOR = {P\k{a}k, Karol},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
VOLUME = {29},
NUMBER = {{\bf 4}},
PAGES = {221--228},
YEAR = {2021},
DOI = {10.2478/forma-2021-0020}
}
@ARTICLE{classes3,
TITLE = {Grothendieck {U}niverses},
AUTHOR = {P\k{a}k, Karol},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
VOLUME = {28},
NUMBER = {{\bf 2}},
PAGES = {211--215},
YEAR = {2020},
DOI = {10.2478/forma-2020-0018}
}
@ARTICLE{aimloop,
TITLE = {{AIM} Loops and the {AIM} Conjecture},
AUTHOR = {Brown, Chad E. and P\k{a}k, Karol},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
VOLUME = {27},
NUMBER = {{\bf 4}},
PAGES = {321--335},
YEAR = {2019},
DOI = {10.2478/forma-2019-0027}
}
@ARTICLE{hilb10_5,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{F}ormalization of the {MRDP} Theorem in the {M}izar System},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2019},
DOI = {10.2478/forma-2019-0020}
VOLUME = {27},
PAGES = {209--222},
NUMBER = {{\bf 2}}}
@ARTICLE{hilb10_5,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{F}ormalization of the {MRDP} Theorem in the {M}izar System},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2019},
DOI = {10.2478/forma-2019-0020}
VOLUME = {27},
PAGES = {209--222},
NUMBER = {{\bf 2}}}
@ARTICLE{hilb10_4,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{D}iophantine Sets. {P}art {II}},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2019},
DOI = {10.2478/forma-2019-0019}
VOLUME = {27},
PAGES = {197--209},
NUMBER = {{\bf 2}}}
@ARTICLE{hilb10_3,
AUTHOR = {Acewicz, Marcin and P\k{a}k, Karol},
TITLE = {Basic Diophantine Relations},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2018},
DOI = {10.2478/forma-2018-0015}
VOLUME = {26},
PAGES = {175--181},
NUMBER = {{\bf 2}}}
@ARTICLE{hilb10_2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Diophantine sets. {P}reliminarie},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2018},
DOI = {10.2478/forma-2018-0007}
VOLUME = {26},
PAGES = {81--90},
NUMBER = {{\bf 1}}}
@ARTICLE{hilb10_1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {The {M}atiyasevich {T}heorem. {P}reliminaries},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2017},
DOI = {10.1515/forma-2017-0029}
VOLUME = {25},
PAGES = {315--325},
NUMBER = {{\bf 4}}}
@ARTICLE{pelle_eq,
AUTHOR = {Acewicz, Marcin and P\k{a}k, Karol},
TITLE = {The {P}ell's {E}quation},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2017},
DOI = {10.1515/forma-2017-0019}
VOLUME = {25},
PAGES = {197--204},
NUMBER = {{\bf 3}}}
@ARTICLE{basel_2,
AUTHOR = {P\k{a}k, Karol and Korni\l{}owicz, Artur },
TITLE = {Basel {P}roblem},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2017},
DOI = {10.1515/forma-2017-0014}
VOLUME = {25},
PAGES = {149--155},
NUMBER = {{\bf 2}}}
@ARTICLE{basel_1,
AUTHOR = {Korni\l{}owicz, Artur and P\k{a}k, Karol},
TITLE = {Basel {P}roblem - {P}reliminaries},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2017},
DOI = {10.1515/forma-2017-00013}
VOLUME = {25},
PAGES = {141--147},
NUMBER = {{\bf 2}}}
@ARTICLE{polyvie1,
AUTHOR = {Korni\l{}owicz, Artur and P\k{a}k, Karol},
TITLE = {Vieta's {F}ormula about the {S}um of {R}oots of {P}olynomials},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2017},
DOI = {10.1515/forma-2017-0008}
VOLUME = {25},
PAGES = {87--92},
NUMBER = {{\bf 2}}}
@ARTICLE{leibniz1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{L}eibniz {S}eries for $\pi$},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2016},
DOI = {10.1515/forma-2016-0023}
VOLUME = {24},
PAGES = {275--280},
NUMBER = {{\bf 4}}}
@ARTICLE{eulrpart,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{E}uler's {P}artition {T}heorem},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2015},
DOI = {10.1515/forma-2015-0009}
VOLUME = {23},
PAGES = {93--99},
NUMBER = {{\bf 2}}}
@ARTICLE{flexary,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{F}lexary {O}perations},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2015},
DOI = {10.1515/forma-2015-0008}
VOLUME = {23},
PAGES = {81--92},
NUMBER = {{\bf 2}}}
@ARTICLE{mfold_0,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{T}opological {M}anifolds},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2014},
DOI = {10.2478/forma-2014-0019}
VOLUME = {22},
PAGES = {179--186},
NUMBER = {{\bf 2}}}
@ARTICLE{ballot_1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{B}ertrand's {B}allot {T}heorem},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2014},
DOI = {10.2478/forma-2014-0014}
VOLUME = {22},
PAGES = {119--123},
NUMBER = {{\bf 2}}}
@ARTICLE{brouwer3,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{B}rouwer {I}nvariance of {D}omain {T}heorem},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2014},
DOI = {10.2478/forma-2014-0003}
VOLUME = {22},
PAGES = {21--28},
NUMBER = {{\bf 1}}}
@ARTICLE{tietze2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{T}ietze {E}xtension {T}heorem for $n$-dimensional {S}paces},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2014},
DOI = {10.2478/forma-2014-0002}
VOLUME = {22},
PAGES = {11--19},
NUMBER = {{\bf 1}}}
@ARTICLE{friends1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{T}he {F}riendship {T}heorem},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2012},
DOI = {10.2478/v10037-012-0028-7},
VOLUME = 20,
PAGES = {235--237},
NUMBER = {{\bf 3}}}
@ARTICLE{matrtop3,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{T}he {R}otation {G}roup},
JOURNAL = {Formalized Mathematics},
ISSN = {1426-2630},
EISSN = {1898-9934},
YEAR = {2012},
DOI = {10.2478/v10037-012-0004-2},
VOLUME = 20,
PAGES = {23--29},
NUMBER = {{\bf 1}}}
@ARTICLE{brouwer2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Brouwer {F}ixed {P}oint {T}heorem in the {G}eneral {C}ase},
JOURNAL = {Formalized Mathematics},
YEAR = {2011},
DOI = {10.2478/v10037-011-0024-3},
VOLUME = 19,
PAGES = {151--153},
NUMBER = {{\bf 3}}}
@ARTICLE{simplex2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{B}rouwer {F}ixed {P}oint {T}heorem for {S}implexes},
JOURNAL = {Formalized Mathematics},
YEAR = {2011},
DOI = {10.2478/v10037-011-0023-4},
VOLUME = 19,
PAGES = {145--150},
NUMBER = {{\bf 3}}}
@ARTICLE{rlaffin3,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Continuity of {B}arycentric {C}oordinates in {E}uclidean {T}opological {S}paces},
JOURNAL = {Formalized Mathematics},
YEAR = {2011},
DOI = {10.2478/v10037-011-0022-5},
VOLUME = 19,
PAGES = {139--144},
NUMBER = {{\bf 3}}}
@ARTICLE{matrtop2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{L}inear {T}ransformations of {E}uclidean {T}opological {S}paces. {P}art {II}},
JOURNAL = {Formalized Mathematics},
YEAR = {2011},
DOI = {10.2478/v10037-011-0017-2},
VOLUME = 19,
PAGES = {109--112},
NUMBER = {{\bf 2}}}
@ARTICLE{matrtop1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{L}inear {T}ransformations of {E}uclidean {T}opological {S}paces},
JOURNAL = {Formalized Mathematics},
YEAR = {2011},
DOI = {10.2478/v10037-011-0016-3},
VOLUME = 19,
PAGES = {103--108},
NUMBER = {{\bf 2}}}
@ARTICLE{simplex1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{S}perner's {L}emma},
JOURNAL = {Formalized Mathematics},
YEAR = {2010},
DOI = {10.2478/v10037-010-0022-x},
VOLUME = 18,
PAGES = {189--196},
NUMBER = {{\bf 4}}}
@ARTICLE{rlaffin2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{T}he {G}eometric {I}nterior in {R}eal {L}inear {S}paces},
JOURNAL = {Formalized Mathematics},
YEAR = {2010},
DOI = {10.2478/v10037-010-0021-y},
VOLUME = 18,
PAGES = {185--188},
NUMBER = {{\bf 3}}}
@ARTICLE{simplex0,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{A}bstract {S}implicial {C}omplexes},
JOURNAL = {Formalized Mathematics},
YEAR = {2010},
DOI = {10.2478/v10037-010-0013-y},
VOLUME = 18,
PAGES = {95--106},
NUMBER = {{\bf 1}}}
@ARTICLE{rlaffin1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {{A}ffine {I}ndependence in {V}ector {S}paces},
JOURNAL = {Formalized Mathematics},
YEAR = {2010},
DOI = {10.2478/v10037-010-0012-z},
VOLUME = 18,
PAGES = {87--93},
NUMBER = {{\bf 1}}}
@ARTICLE{topdim_2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Small {I}nductive {D}imension of {T}opological {S}paces. {P}art {II}},
JOURNAL = {Formalized Mathematics},
YEAR = {2009},
DOI = {10.2478/v10037-009-0027-5},
VOLUME = 17,
PAGES = {219--222},
NUMBER = {{\bf 3}}}
@ARTICLE{topdim_1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Small {I}nductive {D}imension of {T}opological {S}paces},
JOURNAL = {Formalized Mathematics},
YEAR = {2009},
DOI = {10.2478/v10037-009-0025-7},
VOLUME = 17,
PAGES = {207--212},
NUMBER = {{\bf 3}}}
@ARTICLE{metrizts,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Basic {P}roperties of {M}etrizable {T}opological {S}paces},
JOURNAL = {Formalized Mathematics},
YEAR = {2009},
DOI = {10.2478/v10037-009-0024-8},
VOLUME = 17,
PAGES = {201--205},
NUMBER = {{\bf 3}}}
@ARTICLE{matrixj1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Block {D}iagonal {M}atrices},
JOURNAL = {Formalized Mathematics},
YEAR = {2008},
DOI = {10.2478/v10037-008-0031-1},
VOLUME = 16,
PAGES = {259--267},
NUMBER = {{\bf 3}}}
@ARTICLE{vectsp11,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Eigenvalues of a {L}inear {T}ransformation},
JOURNAL = {Formalized Mathematics},
YEAR = {2008},
DOI = {10.2478/v10037-008-0035-x},
VOLUME = 16,
PAGES = {289--295},
NUMBER = {{\bf 4}}}
@ARTICLE{matrlin2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Linear {M}ap of {M}atrices},
JOURNAL = {Formalized Mathematics},
YEAR = {2008},
DOI = {10.2478/v10037-008-0032-0},
VOLUME = 16,
PAGES = {269--275},
NUMBER = {{\bf 3}}}
@ARTICLE{matrixj1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Block {D}iagonal {M}atrices},
JOURNAL = {Formalized Mathematics},
YEAR = {2008},
DOI = {10.2478/v10037-008-0031-1},
VOLUME = 16,
PAGES = {259--267},
NUMBER = {{\bf 3}}}
@ARTICLE{matrix15,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Solutions of {L}inear {E}quations},
JOURNAL = {Formalized Mathematics},
YEAR = {2008},
DOI = {10.2478/v10037-008-0012-4},
VOLUME = 16,
PAGES = {81--90},
NUMBER = {{\bf 1}}}
@ARTICLE{compl_sp,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Complete {S}paces},
JOURNAL = {Formalized Mathematics},
YEAR = {2008},
DOI = {10.2478/v10037-008-0006-2},
VOLUME = 16,
PAGES = {35--43},
NUMBER = {{\bf 1}}}
@ARTICLE{matrix13,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Basic {P}roperties of the {R}ank of {M}atrices over a {F}ield},
JOURNAL = {Formalized Mathematics},
YEAR = {2007},
DOI = {10.2478/v10037-007-0024-5},
VOLUME = 15,
PAGES = {199--211},
NUMBER = {{\bf 4}}}
@ARTICLE{laplace1,
AUTHOR = {P\k{a}k, Karol and Trybulec, Andrzej},
TITLE = {Laplace {E}xpansion},
JOURNAL = {Formalized Mathematics},
YEAR = {2007},
DOI = {10.2478/v10037-007-0016-5},
VOLUME = 15,
PAGES = {143--150},
NUMBER = {{\bf 3}}}
@ARTICLE{matrix11,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Basic {P}roperties of {D}eterminants of {S}quare {M}atrices over a {F}ield},
JOURNAL = {Formalized Mathematics},
YEAR = {2007},
DOI = {10.2478/v10037-007-0003-x},
VOLUME = 15,
PAGES = {17--25},
NUMBER = {{\bf 1}}}
@ARTICLE{catalan2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {The {C}atalan {N}umbers. {P}art {II}},
JOURNAL = {Formalized Mathematics},
YEAR = {2006},
DOI = {10.2478/v10037-006-0019-7},
VOLUME = 14,
PAGES = {153--159},
NUMBER = {{\bf 4}}}
@ARTICLE{card_fin,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Cardinal {N}umbers and {F}inite {S}ets},
JOURNAL = {Formalized Mathematics},
URL = {http://fm.mizar.org/2005-13/pdf13-3/card_fin.pdf},
YEAR = {2005},
VOLUME = 13,
PAGES = {399--406},
NUMBER = {{\bf 3}}}
@ARTICLE{stirl2_1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {Stirling {N}umbers of the {S}econd {K}ind},
JOURNAL = {Formalized Mathematics},
URL = {http://fm.mizar.org/2005-13/pdf13-2/stirl2_1.pdf},
YEAR = {2005},
VOLUME = 13,
PAGES = {337--345},
NUMBER = {{\bf 2}}}
@ARTICLE{nagata_2,
AUTHOR = {P\k{a}k, Karol},
TITLE = {The {N}agata-{S}mirnov {T}heorem. {P}art {II}},
JOURNAL = {Formalized Mathematics},
URL = {http://fm.mizar.org/2004-12/pdf12-3/nagata_2.pdf},
YEAR = {2004},
VOLUME = 12,
PAGES = {385--389},
NUMBER = {{\bf 3}}}
@ARTICLE{nagata_1,
AUTHOR = {P\k{a}k, Karol},
TITLE = {The {N}agata-{S}mirnov {T}heorem. {P}art {I}},
JOURNAL = {Formalized Mathematics},
URL = {http://fm.mizar.org/2004-12/pdf12-3/nagata_1.pdf},
YEAR = {2004},
VOLUME = 12,
PAGES = {341--346},
NUMBER = {{\bf 3}}}