Path	Lines of Code
hollight/valid/aime-1983-p9.ml	3
hollight/valid/aime-1984-p15.ml	24
hollight/valid/aime-1984-p5.ml	6
hollight/valid/algebra-2complexrootspoly-xsqp49eqxp7itxpn7i.ml	1
hollight/valid/algebra-2rootsintpoly-am10tap11eqasqpam110.ml	1
hollight/valid/algebra-2rootspoly-apatapbeq2asqp2ab.ml	1
hollight/valid/algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.ml	6
hollight/valid/algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.ml	1
hollight/valid/algebra-amgm-faxinrrp2msqrt2geq2mxm1div2x.ml	5
hollight/valid/algebra-amgm-prod1toneq1-sum1tongeqn.ml	6
hollight/valid/algebra-amgm-sqrtxymulxmyeqxpy-xpygeq4.ml	7
hollight/valid/algebra-amgm-sumasqdivbsqgeqsumbdiva.ml	5
hollight/valid/algebra-binomnegdiscrineq-10alt28asqp1.ml	1
hollight/valid/algebra-manipexpr-2erprsqpesqeqnrpnesq.ml	1
hollight/valid/algebra-manipexpr-apbeq2cceqiacpbceqm2.ml	6
hollight/valid/algebra-sqineq-2at2pclta2c2p41pc.ml	1
hollight/valid/algebra-sqineq-2unitcircatblt1.ml	1
hollight/valid/algebra-sqineq-36azm9asqle36zsq.ml	1
hollight/valid/algebra-sqineq-4bap1lt4bsqpap1sq.ml	1
hollight/valid/amc12-2000-p11.ml	4
hollight/valid/amc12-2000-p15.ml	6
hollight/valid/amc12-2000-p5.ml	6
hollight/valid/amc12-2001-p2.ml	6
hollight/valid/amc12-2001-p9.ml	6
hollight/valid/amc12a-2002-p1.ml	6
hollight/valid/amc12a-2002-p12.ml	6
hollight/valid/amc12a-2002-p21.ml	7
hollight/valid/amc12a-2003-p1.ml	6
hollight/valid/amc12a-2003-p24.ml	4
hollight/valid/amc12a-2003-p25.ml	7
hollight/valid/amc12a-2020-p13.ml	8
hollight/valid/amc12a-2020-p22.ml	1
hollight/valid/amc12a-2021-p7.ml	1
hollight/valid/amc12b-2002-p11.ml	6
hollight/valid/amc12b-2002-p3.ml	6
hollight/valid/amc12b-2002-p6.ml	4
hollight/valid/amc12b-2003-p17.ml	7
hollight/valid/amc12b-2003-p6.ml	7
hollight/valid/amc12b-2003-p9.ml	4
hollight/valid/amc12b-2004-p3.ml	1
hollight/valid/amc12b-2020-p5.ml	7
hollight/valid/amc12b-2021-p21.ml	5
hollight/valid/imo-1990-p3.ml	4
hollight/valid/imo-2006-a6.ml	5
hollight/valid/induction-divisibility-3div2tooddnp1.ml	1
hollight/valid/induction-divisibility-3divnto3m2n.ml	1
hollight/valid/induction-divisibility-9div10tonm1.ml	1
hollight/valid/induction-ineq-nsqlefactn.ml	1
hollight/valid/induction-seq-mul2pnp1.ml	6
hollight/valid/induction-sum-1oktkp1.ml	1
hollight/valid/induction-sum-odd.ml	1
hollight/valid/induction-sum2kp1npqsqm1.ml	1
hollight/valid/mathd-algebra-10.ml	1
hollight/valid/mathd-algebra-101.ml	1
hollight/valid/mathd-algebra-104.ml	5
hollight/valid/mathd-algebra-109.ml	6
hollight/valid/mathd-algebra-11.ml	7
hollight/valid/mathd-algebra-110.ml	6
hollight/valid/mathd-algebra-116.ml	6
hollight/valid/mathd-algebra-119.ml	6
hollight/valid/mathd-algebra-123.ml	7
hollight/valid/mathd-algebra-126.ml	7
hollight/valid/mathd-algebra-13.ml	5
hollight/valid/mathd-algebra-131.ml	8
hollight/valid/mathd-algebra-132.ml	7
hollight/valid/mathd-algebra-140.ml	6
hollight/valid/mathd-algebra-144.ml	9
hollight/valid/mathd-algebra-149.ml	7
hollight/valid/mathd-algebra-15.ml	5
hollight/valid/mathd-algebra-151.ml	6
hollight/valid/mathd-algebra-159.ml	6
hollight/valid/mathd-algebra-181.ml	6
hollight/valid/mathd-algebra-182.ml	1
hollight/valid/mathd-algebra-185.ml	6
hollight/valid/mathd-algebra-190.ml	1
hollight/valid/mathd-algebra-192.ml	7
hollight/valid/mathd-algebra-206.ml	8
hollight/valid/mathd-algebra-214.ml	6
hollight/valid/mathd-algebra-22.ml	1
hollight/valid/mathd-algebra-224.ml	1
hollight/valid/mathd-algebra-234.ml	5
hollight/valid/mathd-algebra-245.ml	5
hollight/valid/mathd-algebra-247.ml	7
hollight/valid/mathd-algebra-251.ml	6
hollight/valid/mathd-algebra-267.ml	7
hollight/valid/mathd-algebra-28.ml	6
hollight/valid/mathd-algebra-282.ml	12
hollight/valid/mathd-algebra-327.ml	5
hollight/valid/mathd-algebra-35.ml	6
hollight/valid/mathd-algebra-37.ml	6
hollight/valid/mathd-algebra-421.ml	9
hollight/valid/mathd-algebra-43.ml	7
hollight/valid/mathd-algebra-455.ml	5
hollight/valid/mathd-algebra-48.ml	6
hollight/valid/mathd-algebra-51.ml	7
hollight/valid/mathd-algebra-55.ml	6
hollight/valid/mathd-algebra-59.ml	1
hollight/valid/mathd-algebra-67.ml	5
hollight/valid/mathd-algebra-69.ml	7
hollight/valid/mathd-algebra-73.ml	6
hollight/valid/mathd-algebra-77.ml	8
hollight/valid/mathd-algebra-89.ml	5
hollight/valid/mathd-algebra-96.ml	8
hollight/valid/mathd-numbertheory-101.ml	1
hollight/valid/mathd-numbertheory-102.ml	1
hollight/valid/mathd-numbertheory-109.ml	1
hollight/valid/mathd-numbertheory-110.ml	7
hollight/valid/mathd-numbertheory-126.ml	14
hollight/valid/mathd-numbertheory-13.ml	10
hollight/valid/mathd-numbertheory-132.ml	1
hollight/valid/mathd-numbertheory-133.ml	1
hollight/valid/mathd-numbertheory-136.ml	1
hollight/valid/mathd-numbertheory-149.ml	1
hollight/valid/mathd-numbertheory-155.ml	1
hollight/valid/mathd-numbertheory-156.ml	5
hollight/valid/mathd-numbertheory-169.ml	1
hollight/valid/mathd-numbertheory-198.ml	1
hollight/valid/mathd-numbertheory-200.ml	1
hollight/valid/mathd-numbertheory-202.ml	1
hollight/valid/mathd-numbertheory-211.ml	1
hollight/valid/mathd-numbertheory-22.ml	6
hollight/valid/mathd-numbertheory-221.ml	1
hollight/valid/mathd-numbertheory-232.ml	10
hollight/valid/mathd-numbertheory-236.ml	1
hollight/valid/mathd-numbertheory-24.ml	1
hollight/valid/mathd-numbertheory-252.ml	1
hollight/valid/mathd-numbertheory-257.ml	6
hollight/valid/mathd-numbertheory-284.ml	6
hollight/valid/mathd-numbertheory-30.ml	1
hollight/valid/mathd-numbertheory-301.ml	5
hollight/valid/mathd-numbertheory-303.ml	1
hollight/valid/mathd-numbertheory-32.ml	1
hollight/valid/mathd-numbertheory-326.ml	5
hollight/valid/mathd-numbertheory-33.ml	6
hollight/valid/mathd-numbertheory-335.ml	5
hollight/valid/mathd-numbertheory-35.ml	5
hollight/valid/mathd-numbertheory-37.ml	1
hollight/valid/mathd-numbertheory-370.ml	5
hollight/valid/mathd-numbertheory-403.ml	1
hollight/valid/mathd-numbertheory-405.ml	10
hollight/valid/mathd-numbertheory-412.ml	6
hollight/valid/mathd-numbertheory-42.ml	10
hollight/valid/mathd-numbertheory-43.ml	6
hollight/valid/mathd-numbertheory-45.ml	1
hollight/valid/mathd-numbertheory-458.ml	5
hollight/valid/mathd-numbertheory-466.ml	1
hollight/valid/mathd-numbertheory-48.ml	6
hollight/valid/mathd-numbertheory-530.ml	7
hollight/valid/mathd-numbertheory-629.ml	1
hollight/valid/mathd-numbertheory-64.ml	8
hollight/valid/mathd-numbertheory-640.ml	1
hollight/valid/mathd-numbertheory-668.ml	14
hollight/valid/mathd-numbertheory-690.ml	8
hollight/valid/mathd-numbertheory-709.ml	7
hollight/valid/mathd-numbertheory-739.ml	1
hollight/valid/mathd-numbertheory-81.ml	1
hollight/valid/mathd-numbertheory-84.ml	1
hollight/valid/mathd-numbertheory-92.ml	5
hollight/valid/numbertheory-2dvd4expn.ml	1
hollight/valid/numbertheory-prmdvsneqnsqmodpeq0.ml	7
hollight/valid/numbertheory-sqmod3in01d.ml	4
hollight/valid/numbertheory-sqmod4in01d.ml	4
hollight/valid/numbertheory-xsqpysqintdenomeq.ml	6
isabelle/valid/aimeII_2020_p6.thy	14
isabelle/valid/aimeI_2000_p7.thy	19
isabelle/valid/aimeI_2001_p3.thy	16
isabelle/valid/aime_1983_p9.thy	24
isabelle/valid/aime_1984_p15.thy	18
isabelle/valid/aime_1984_p5.thy	12
isabelle/valid/aime_1987_p8.thy	13
isabelle/valid/aime_1988_p3.thy	13
isabelle/valid/aime_1988_p4.thy	14
isabelle/valid/aime_1990_p2.thy	11
isabelle/valid/aime_1991_p1.thy	14
isabelle/valid/aime_1991_p6.thy	13
isabelle/valid/aime_1994_p4.thy	13
isabelle/valid/aime_1996_p5.thy	20
isabelle/valid/aime_1997_p12.thy	12
isabelle/valid/algebra_2complexrootspoly_xsqp49eqxp7itxpn7i.thy	11
isabelle/valid/algebra_2rootsintpoly_am10tap11eqasqpam110.thy	19
isabelle/valid/algebra_2rootspoly_apatapbeq2asqp2ab.thy	11
isabelle/valid/algebra_2varlineareq_xpeeq7_2xpeeq3_eeq11_xeqn4.thy	18
isabelle/valid/algebra_3rootspoly_amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.thy	11
isabelle/valid/algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x.thy	10
isabelle/valid/algebra_amgm_prod1toneq1_sum1tongeqn.thy	14
isabelle/valid/algebra_amgm_sqrtxymulxmyeqxpy_xpygeq4.thy	14
isabelle/valid/algebra_amgm_sumasqdivbsqgeqsumbdiva.thy	12
isabelle/valid/algebra_apb4leq8ta4pb4.thy	12
isabelle/valid/algebra_binomnegdiscrineq_10alt28asqp1.thy	11
isabelle/valid/algebra_manipexpr_2erprsqpesqeqnrpnesq.thy	11
isabelle/valid/algebra_manipexpr_apbeq2cceqiacpbceqm2.thy	13
isabelle/valid/algebra_sqineq_2at2pclta2c2p41pc.thy	11
isabelle/valid/algebra_sqineq_2unitcircatblt1.thy	24
isabelle/valid/algebra_sqineq_36azm9asqle36zsq.thy	11
isabelle/valid/algebra_sqineq_4bap1lt4bsqpap1sq.thy	11
isabelle/valid/algebra_xmysqpymzsqpzmxsqeqxyz_xpypzp6dvdx3y3z3.thy	12
isabelle/valid/amc12_2000_p11.thy	14
isabelle/valid/amc12_2000_p15.thy	14
isabelle/valid/amc12_2000_p5.thy	12
isabelle/valid/amc12_2001_p2.thy	15
isabelle/valid/amc12_2001_p9.thy	20
isabelle/valid/amc12a_2002_p1.thy	14
isabelle/valid/amc12a_2002_p12.thy	15
isabelle/valid/amc12a_2002_p21.thy	15
isabelle/valid/amc12a_2003_p1.thy	23
isabelle/valid/amc12a_2003_p24.thy	35
isabelle/valid/amc12a_2003_p25.thy	14
isabelle/valid/amc12a_2008_p15.thy	12
isabelle/valid/amc12a_2008_p2.thy	16
isabelle/valid/amc12a_2008_p4.thy	10
isabelle/valid/amc12a_2008_p8.thy	19
isabelle/valid/amc12a_2009_p15.thy	14
isabelle/valid/amc12a_2009_p2.thy	10
isabelle/valid/amc12a_2009_p25.thy	14
isabelle/valid/amc12a_2009_p5.thy	22
isabelle/valid/amc12a_2009_p9.thy	14
isabelle/valid/amc12a_2010_p10.thy	17
isabelle/valid/amc12a_2010_p11.thy	14
isabelle/valid/amc12a_2010_p22.thy	11
isabelle/valid/amc12a_2011_p18.thy	12
isabelle/valid/amc12a_2013_p7.thy	19
isabelle/valid/amc12a_2013_p8.thy	29
isabelle/valid/amc12a_2015_p10.thy	14
isabelle/valid/amc12a_2016_p2.thy	12
isabelle/valid/amc12a_2016_p3.thy	12
isabelle/valid/amc12a_2017_p2.thy	14
isabelle/valid/amc12a_2017_p7.thy	14
isabelle/valid/amc12a_2019_p21.thy	12
isabelle/valid/amc12a_2019_p9.thy	15
isabelle/valid/amc12a_2020_p13.thy	15
isabelle/valid/amc12a_2020_p22.thy	12
isabelle/valid/amc12a_2021_p7.thy	12
isabelle/valid/amc12b_2002_p11.thy	14
isabelle/valid/amc12b_2002_p3.thy	31
isabelle/valid/amc12b_2002_p6.thy	16
isabelle/valid/amc12b_2003_p17.thy	22
isabelle/valid/amc12b_2003_p6.thy	14
isabelle/valid/amc12b_2003_p9.thy	13
isabelle/valid/amc12b_2004_p3.thy	12
isabelle/valid/amc12b_2020_p5.thy	13
isabelle/valid/amc12b_2021_p21.thy	13
isabelle/valid/imo_1961_p1.thy	18
isabelle/valid/imo_1962_p4.thy	14
isabelle/valid/imo_1964_p1_1.thy	12
isabelle/valid/imo_1964_p1_2.thy	11
isabelle/valid/imo_1965_p1.thy	17
isabelle/valid/imo_1966_p4.thy	14
isabelle/valid/imo_1966_p5.thy	21
isabelle/valid/imo_1967_p3.thy	16
isabelle/valid/imo_1973_p3.thy	12
isabelle/valid/imo_1974_p5.thy	12
isabelle/valid/imo_1977_p5.thy	14
isabelle/valid/imo_1978_p5.thy	16
isabelle/valid/imo_1979_p1.thy	14
isabelle/valid/imo_1984_p2.thy	16
isabelle/valid/imo_1987_p4.thy	11
isabelle/valid/imo_1987_p6.thy	15
isabelle/valid/imo_1988_p6.thy	13
isabelle/valid/imo_1990_p3.thy	13
isabelle/valid/imo_1993_p5.thy	12
isabelle/valid/imo_2006_p6.thy	12
isabelle/valid/induction_divisibility_3div2tooddnp1.thy	23
isabelle/valid/induction_divisibility_3divnto3m2n.thy	12
isabelle/valid/induction_divisibility_9div10tonm1.thy	12
isabelle/valid/induction_ineq_nsqlefactn.thy	44
isabelle/valid/induction_seq_mul2pnp1.thy	14
isabelle/valid/induction_sum2kp1npqsqm1.thy	12
isabelle/valid/induction_sum_1oktkp1.thy	11
isabelle/valid/induction_sum_odd.thy	12
isabelle/valid/mathd_algebra_10.thy	10
isabelle/valid/mathd_algebra_101.thy	25
isabelle/valid/mathd_algebra_104.thy	15
isabelle/valid/mathd_algebra_109.thy	13
isabelle/valid/mathd_algebra_11.thy	26
isabelle/valid/mathd_algebra_110.thy	13
isabelle/valid/mathd_algebra_116.thy	13
isabelle/valid/mathd_algebra_119.thy	13
isabelle/valid/mathd_algebra_123.thy	18
isabelle/valid/mathd_algebra_126.thy	17
isabelle/valid/mathd_algebra_13.thy	13
isabelle/valid/mathd_algebra_131.thy	16
isabelle/valid/mathd_algebra_132.thy	24
isabelle/valid/mathd_algebra_140.thy	13
isabelle/valid/mathd_algebra_144.thy	15
isabelle/valid/mathd_algebra_149.thy	14
isabelle/valid/mathd_algebra_15.thy	15
isabelle/valid/mathd_algebra_151.thy	11
isabelle/valid/mathd_algebra_159.thy	19
isabelle/valid/mathd_algebra_181.thy	20
isabelle/valid/mathd_algebra_182.thy	11
isabelle/valid/mathd_algebra_185.thy	12
isabelle/valid/mathd_algebra_190.thy	10
isabelle/valid/mathd_algebra_192.thy	15
isabelle/valid/mathd_algebra_206.thy	16
isabelle/valid/mathd_algebra_214.thy	18
isabelle/valid/mathd_algebra_22.thy	10
isabelle/valid/mathd_algebra_224.thy	11
isabelle/valid/mathd_algebra_234.thy	20
isabelle/valid/mathd_algebra_245.thy	36
isabelle/valid/mathd_algebra_247.thy	20
isabelle/valid/mathd_algebra_251.thy	13
isabelle/valid/mathd_algebra_267.thy	14
isabelle/valid/mathd_algebra_28.thy	14
isabelle/valid/mathd_algebra_282.thy	13
isabelle/valid/mathd_algebra_31.thy	14
isabelle/valid/mathd_algebra_323.thy	13
isabelle/valid/mathd_algebra_327.thy	12
isabelle/valid/mathd_algebra_35.thy	17
isabelle/valid/mathd_algebra_37.thy	17
isabelle/valid/mathd_algebra_393.thy	13
isabelle/valid/mathd_algebra_405.thy	27
isabelle/valid/mathd_algebra_410.thy	12
isabelle/valid/mathd_algebra_421.thy	16
isabelle/valid/mathd_algebra_422.thy	25
isabelle/valid/mathd_algebra_43.thy	22
isabelle/valid/mathd_algebra_433.thy	16
isabelle/valid/mathd_algebra_437.thy	16
isabelle/valid/mathd_algebra_451.thy	16
isabelle/valid/mathd_algebra_455.thy	17
isabelle/valid/mathd_algebra_462.thy	10
isabelle/valid/mathd_algebra_48.thy	14
isabelle/valid/mathd_algebra_480.thy	19
isabelle/valid/mathd_algebra_482.thy	19
isabelle/valid/mathd_algebra_493.thy	15
isabelle/valid/mathd_algebra_509.thy	10
isabelle/valid/mathd_algebra_51.thy	13
isabelle/valid/mathd_algebra_510.thy	13
isabelle/valid/mathd_algebra_536.thy	11
isabelle/valid/mathd_algebra_547.thy	15
isabelle/valid/mathd_algebra_55.thy	17
isabelle/valid/mathd_algebra_568.thy	11
isabelle/valid/mathd_algebra_59.thy	17
isabelle/valid/mathd_algebra_616.thy	16
isabelle/valid/mathd_algebra_67.thy	16
isabelle/valid/mathd_algebra_69.thy	13
isabelle/valid/mathd_algebra_73.thy	13
isabelle/valid/mathd_algebra_77.thy	16
isabelle/valid/mathd_algebra_89.thy	12
isabelle/valid/mathd_algebra_96.thy	15
isabelle/valid/mathd_numbertheory_101.thy	10
isabelle/valid/mathd_numbertheory_102.thy	10
isabelle/valid/mathd_numbertheory_109.thy	12
isabelle/valid/mathd_numbertheory_110.thy	14
isabelle/valid/mathd_numbertheory_126.thy	16
isabelle/valid/mathd_numbertheory_13.thy	18
isabelle/valid/mathd_numbertheory_132.thy	10
isabelle/valid/mathd_numbertheory_136.thy	11
isabelle/valid/mathd_numbertheory_149.thy	11
isabelle/valid/mathd_numbertheory_155.thy	10
isabelle/valid/mathd_numbertheory_156.thy	12
isabelle/valid/mathd_numbertheory_169.thy	10
isabelle/valid/mathd_numbertheory_188.thy	10
isabelle/valid/mathd_numbertheory_198.thy	10
isabelle/valid/mathd_numbertheory_200.thy	10
isabelle/valid/mathd_numbertheory_202.thy	10
isabelle/valid/mathd_numbertheory_211.thy	11
isabelle/valid/mathd_numbertheory_22.thy	13
isabelle/valid/mathd_numbertheory_221.thy	11
isabelle/valid/mathd_numbertheory_232.thy	16
isabelle/valid/mathd_numbertheory_236.thy	10
isabelle/valid/mathd_numbertheory_24.thy	10
isabelle/valid/mathd_numbertheory_252.thy	10
isabelle/valid/mathd_numbertheory_257.thy	13
isabelle/valid/mathd_numbertheory_269.thy	10
isabelle/valid/mathd_numbertheory_284.thy	20
isabelle/valid/mathd_numbertheory_30.thy	10
isabelle/valid/mathd_numbertheory_301.thy	13
isabelle/valid/mathd_numbertheory_303.thy	11
isabelle/valid/mathd_numbertheory_32.thy	11
isabelle/valid/mathd_numbertheory_326.thy	12
isabelle/valid/mathd_numbertheory_33.thy	13
isabelle/valid/mathd_numbertheory_335.thy	18
isabelle/valid/mathd_numbertheory_35.thy	11
isabelle/valid/mathd_numbertheory_37.thy	10
isabelle/valid/mathd_numbertheory_370.thy	12
isabelle/valid/mathd_numbertheory_403.thy	11
isabelle/valid/mathd_numbertheory_405.thy	18
isabelle/valid/mathd_numbertheory_412.thy	13
isabelle/valid/mathd_numbertheory_42.thy	16
isabelle/valid/mathd_numbertheory_43.thy	13
isabelle/valid/mathd_numbertheory_45.thy	8
isabelle/valid/mathd_numbertheory_458.thy	12
isabelle/valid/mathd_numbertheory_461.thy	13
isabelle/valid/mathd_numbertheory_466.thy	11
isabelle/valid/mathd_numbertheory_48.thy	13
isabelle/valid/mathd_numbertheory_530.thy	14
isabelle/valid/mathd_numbertheory_543.thy	10
isabelle/valid/mathd_numbertheory_629.thy	10
isabelle/valid/mathd_numbertheory_64.thy	11
isabelle/valid/mathd_numbertheory_640.thy	10
isabelle/valid/mathd_numbertheory_668.thy	15
isabelle/valid/mathd_numbertheory_690.thy	12
isabelle/valid/mathd_numbertheory_709.thy	15
isabelle/valid/mathd_numbertheory_739.thy	10
isabelle/valid/mathd_numbertheory_780.thy	15
isabelle/valid/mathd_numbertheory_81.thy	10
isabelle/valid/mathd_numbertheory_84.thy	10
isabelle/valid/mathd_numbertheory_92.thy	12
isabelle/valid/mathd_numbertheory_961.thy	10
isabelle/valid/numbertheory_2dvd4expn.thy	12
isabelle/valid/numbertheory_aneqprodakp4_anmsqrtanp1eq2.thy	13
isabelle/valid/numbertheory_nckeqnm1ckpnm1ckm1.thy	14
isabelle/valid/numbertheory_prmdvsneqnsqmodpeq0.thy	13
isabelle/valid/numbertheory_sqmod3in01d.thy	11
isabelle/valid/numbertheory_sqmod4in01d.thy	11
isabelle/valid/numbertheory_sumkmulnckeqnmul2pownm1.thy	14
isabelle/valid/numbertheory_xsqpysqintdenomeq.thy	13
lean/scripts/lint_style.py	234
lean/src/minif2f_import.lean	87
lean/src/valid.lean	2132
leanpkg.toml	7
metamath/valid/aime-1983-p9.mm	9
metamath/valid/aime-1984-p15.mm	15
metamath/valid/aime-1984-p5.mm	11
metamath/valid/aime-1987-p8.mm	9
metamath/valid/aime-1988-p3.mm	9
metamath/valid/aime-1988-p4.mm	11
metamath/valid/aime-1990-p2.mm	7
metamath/valid/aime-1991-p1.mm	11
metamath/valid/aime-1991-p6.mm	9
metamath/valid/aime-1994-p4.mm	9
metamath/valid/aime-1996-p5.mm	21
metamath/valid/aime-1997-p12.mm	9
metamath/valid/aimeI-2000-p7.mm	16
metamath/valid/aimeI-2001-p3.mm	15
metamath/valid/aimeII-2020-p6.mm	13
metamath/valid/algebra-2complexrootspoly-xsqp49eqxp7itxpn7i.mm	20
metamath/valid/algebra-2rootsintpoly-am10tap11eqasqpam110.mm	19
metamath/valid/algebra-2rootspoly-apatapbeq2asqp2ab.mm	12
metamath/valid/algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.mm	31
metamath/valid/algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.mm	25
metamath/valid/algebra-amgm-faxinrrp2msqrt2geq2mxm1div2x.mm	7
metamath/valid/algebra-amgm-prod1toneq1-sum1tongeqn.mm	10
metamath/valid/algebra-amgm-sqrtxymulxmyeqxpy-xpygeq4.mm	11
metamath/valid/algebra-amgm-sumasqdivbsqgeqsumbdiva.mm	10
metamath/valid/algebra-apb4leq8ta4pb4.mm	9
metamath/valid/algebra-binomnegdiscrineq-10alt28asqp1.mm	23
metamath/valid/algebra-manipexpr-2erprsqpesqeqnrpnesq.mm	14
metamath/valid/algebra-manipexpr-apbeq2cceqiacpbceqm2.mm	16
metamath/valid/algebra-sqineq-2at2pclta2c2p41pc.mm	31
metamath/valid/algebra-sqineq-2unitcircatblt1.mm	10
metamath/valid/algebra-sqineq-36azm9asqle36zsq.mm	25
metamath/valid/algebra-sqineq-4bap1lt4bsqpap1sq.mm	34
metamath/valid/algebra-xmysqpymzsqpzmxsqeqxyz-xpypzp6dvdx3y3z3.mm	11
metamath/valid/amc12-2000-p11.mm	29
metamath/valid/amc12-2000-p15.mm	10
metamath/valid/amc12-2000-p5.mm	20
metamath/valid/amc12-2001-p2.mm	18
metamath/valid/amc12-2001-p9.mm	28
metamath/valid/amc12a-2002-p1.mm	12
metamath/valid/amc12a-2002-p12.mm	6
metamath/valid/amc12a-2002-p21.mm	11
metamath/valid/amc12a-2003-p1.mm	25
metamath/valid/amc12a-2003-p24.mm	31
metamath/valid/amc12a-2003-p25.mm	9
metamath/valid/amc12a-2008-p15.mm	9
metamath/valid/amc12a-2008-p2.mm	9
metamath/valid/amc12a-2008-p4.mm	7
metamath/valid/amc12a-2008-p8.mm	11
metamath/valid/amc12a-2009-p15.mm	9
metamath/valid/amc12a-2009-p2.mm	7
metamath/valid/amc12a-2009-p25.mm	11
metamath/valid/amc12a-2009-p5.mm	9
metamath/valid/amc12a-2009-p9.mm	14
metamath/valid/amc12a-2010-p10.mm	15
metamath/valid/amc12a-2010-p11.mm	11
metamath/valid/amc12a-2010-p22.mm	8
metamath/valid/amc12a-2011-p18.mm	10
metamath/valid/amc12a-2013-p7.mm	11
metamath/valid/amc12a-2013-p8.mm	13
metamath/valid/amc12a-2015-p10.mm	12
metamath/valid/amc12a-2016-p2.mm	9
metamath/valid/amc12a-2016-p3.mm	9
metamath/valid/amc12a-2017-p2.mm	12
metamath/valid/amc12a-2017-p7.mm	11
metamath/valid/amc12a-2019-p21.mm	9
metamath/valid/amc12a-2019-p9.mm	11
metamath/valid/amc12a-2020-p13.mm	16
metamath/valid/amc12a-2020-p22.mm	8
metamath/valid/amc12a-2021-p7.mm	9
metamath/valid/amc12b-2002-p11.mm	13
metamath/valid/amc12b-2002-p3.mm	34
metamath/valid/amc12b-2002-p6.mm	12
metamath/valid/amc12b-2003-p17.mm	27
metamath/valid/amc12b-2003-p6.mm	43
metamath/valid/amc12b-2003-p9.mm	36
metamath/valid/amc12b-2004-p3.mm	53
metamath/valid/amc12b-2020-p5.mm	11
metamath/valid/amc12b-2021-p21.mm	8
metamath/valid/imo-1961-p1.mm	18
metamath/valid/imo-1962-p4.mm	9
metamath/valid/imo-1964-p1-1.mm	9
metamath/valid/imo-1964-p1-2.mm	8
metamath/valid/imo-1965-p1.mm	12
metamath/valid/imo-1966-p4.mm	10
metamath/valid/imo-1966-p5.mm	19
metamath/valid/imo-1967-p3.mm	13
metamath/valid/imo-1973-p3.mm	10
metamath/valid/imo-1974-p5.mm	13
metamath/valid/imo-1977-p5.mm	14
metamath/valid/imo-1978-p5.mm	9
metamath/valid/imo-1979-p1.mm	10
metamath/valid/imo-1984-p2.mm	13
metamath/valid/imo-1987-p4.mm	8
metamath/valid/imo-1987-p6.mm	12
metamath/valid/imo-1988-p6.mm	10
metamath/valid/imo-1990-p3.mm	9
metamath/valid/imo-1993-p5.mm	7
metamath/valid/imo-2006-p6.mm	10
metamath/valid/induction-divisibility-3div2tooddnp1.mm	32
metamath/valid/induction-divisibility-3divnto3m2n.mm	43
metamath/valid/induction-divisibility-9div10tonm1.mm	25
metamath/valid/induction-ineq-nsqlefactn.mm	37
metamath/valid/induction-seq-mul2pnp1.mm	51
metamath/valid/induction-sum-1oktkp1.mm	40
metamath/valid/induction-sum-odd.mm	28
metamath/valid/induction-sum2kp1npqsqm1.mm	33
metamath/valid/mathd-algebra-10.mm	7
metamath/valid/mathd-algebra-101.mm	9
metamath/valid/mathd-algebra-104.mm	9
metamath/valid/mathd-algebra-109.mm	11
metamath/valid/mathd-algebra-11.mm	12
metamath/valid/mathd-algebra-110.mm	9
metamath/valid/mathd-algebra-116.mm	10
metamath/valid/mathd-algebra-119.mm	11
metamath/valid/mathd-algebra-123.mm	11
metamath/valid/mathd-algebra-126.mm	11
metamath/valid/mathd-algebra-13.mm	10
metamath/valid/mathd-algebra-131.mm	13
metamath/valid/mathd-algebra-132.mm	11
metamath/valid/mathd-algebra-140.mm	12
metamath/valid/mathd-algebra-144.mm	15
metamath/valid/mathd-algebra-149.mm	7
metamath/valid/mathd-algebra-15.mm	8
metamath/valid/mathd-algebra-151.mm	28
metamath/valid/mathd-algebra-159.mm	34
metamath/valid/mathd-algebra-181.mm	10
metamath/valid/mathd-algebra-182.mm	8
metamath/valid/mathd-algebra-185.mm	8
metamath/valid/mathd-algebra-190.mm	7
metamath/valid/mathd-algebra-192.mm	23
metamath/valid/mathd-algebra-206.mm	13
metamath/valid/mathd-algebra-214.mm	10
metamath/valid/mathd-algebra-22.mm	7
metamath/valid/mathd-algebra-224.mm	7
metamath/valid/mathd-algebra-234.mm	9
metamath/valid/mathd-algebra-245.mm	36
metamath/valid/mathd-algebra-247.mm	18
metamath/valid/mathd-algebra-251.mm	14
metamath/valid/mathd-algebra-267.mm	11
metamath/valid/mathd-algebra-28.mm	10
metamath/valid/mathd-algebra-282.mm	10
metamath/valid/mathd-algebra-31.mm	40
metamath/valid/mathd-algebra-323.mm	9
metamath/valid/mathd-algebra-327.mm	9
metamath/valid/mathd-algebra-35.mm	9
metamath/valid/mathd-algebra-37.mm	11
metamath/valid/mathd-algebra-393.mm	7
metamath/valid/mathd-algebra-405.mm	9
metamath/valid/mathd-algebra-410.mm	10
metamath/valid/mathd-algebra-421.mm	16
metamath/valid/mathd-algebra-422.mm	5
metamath/valid/mathd-algebra-43.mm	12
metamath/valid/mathd-algebra-433.mm	8
metamath/valid/mathd-algebra-437.mm	14
metamath/valid/mathd-algebra-451.mm	5
metamath/valid/mathd-algebra-455.mm	17
metamath/valid/mathd-algebra-462.mm	7
metamath/valid/mathd-algebra-48.mm	9
metamath/valid/mathd-algebra-480.mm	12
metamath/valid/mathd-algebra-482.mm	14
metamath/valid/mathd-algebra-493.mm	8
metamath/valid/mathd-algebra-509.mm	7
metamath/valid/mathd-algebra-51.mm	11
metamath/valid/mathd-algebra-510.mm	11
metamath/valid/mathd-algebra-536.mm	7
metamath/valid/mathd-algebra-547.mm	9
metamath/valid/mathd-algebra-55.mm	9
metamath/valid/mathd-algebra-568.mm	8
metamath/valid/mathd-algebra-59.mm	9
metamath/valid/mathd-algebra-616.mm	9
metamath/valid/mathd-algebra-67.mm	9
metamath/valid/mathd-algebra-69.mm	11
metamath/valid/mathd-algebra-73.mm	13
metamath/valid/mathd-algebra-77.mm	12
metamath/valid/mathd-algebra-89.mm	8
metamath/valid/mathd-algebra-96.mm	14
metamath/valid/mathd-numbertheory-101.mm	7
metamath/valid/mathd-numbertheory-102.mm	7
metamath/valid/mathd-numbertheory-109.mm	8
metamath/valid/mathd-numbertheory-110.mm	12
metamath/valid/mathd-numbertheory-126.mm	12
metamath/valid/mathd-numbertheory-13.mm	14
metamath/valid/mathd-numbertheory-132.mm	7
metamath/valid/mathd-numbertheory-136.mm	9
metamath/valid/mathd-numbertheory-149.mm	7
metamath/valid/mathd-numbertheory-155.mm	7
metamath/valid/mathd-numbertheory-156.mm	8
metamath/valid/mathd-numbertheory-169.mm	7
metamath/valid/mathd-numbertheory-188.mm	14
metamath/valid/mathd-numbertheory-198.mm	7
metamath/valid/mathd-numbertheory-200.mm	7
metamath/valid/mathd-numbertheory-202.mm	7
metamath/valid/mathd-numbertheory-211.mm	8
metamath/valid/mathd-numbertheory-22.mm	10
metamath/valid/mathd-numbertheory-221.mm	7
metamath/valid/mathd-numbertheory-232.mm	16
metamath/valid/mathd-numbertheory-236.mm	7
metamath/valid/mathd-numbertheory-24.mm	7
metamath/valid/mathd-numbertheory-252.mm	7
metamath/valid/mathd-numbertheory-257.mm	9
metamath/valid/mathd-numbertheory-269.mm	7
metamath/valid/mathd-numbertheory-284.mm	10
metamath/valid/mathd-numbertheory-30.mm	7
metamath/valid/mathd-numbertheory-301.mm	8
metamath/valid/mathd-numbertheory-303.mm	7
metamath/valid/mathd-numbertheory-32.mm	7
metamath/valid/mathd-numbertheory-326.mm	9
metamath/valid/mathd-numbertheory-33.mm	10
metamath/valid/mathd-numbertheory-335.mm	9
metamath/valid/mathd-numbertheory-35.mm	7
metamath/valid/mathd-numbertheory-37.mm	7
metamath/valid/mathd-numbertheory-370.mm	9
metamath/valid/mathd-numbertheory-403.mm	7
metamath/valid/mathd-numbertheory-405.mm	17
metamath/valid/mathd-numbertheory-412.mm	11
metamath/valid/mathd-numbertheory-42.mm	14
metamath/valid/mathd-numbertheory-43.mm	10
metamath/valid/mathd-numbertheory-45.mm	7
metamath/valid/mathd-numbertheory-458.mm	9
metamath/valid/mathd-numbertheory-461.mm	8
metamath/valid/mathd-numbertheory-466.mm	7
metamath/valid/mathd-numbertheory-48.mm	10
metamath/valid/mathd-numbertheory-530.mm	11
metamath/valid/mathd-numbertheory-543.mm	7
metamath/valid/mathd-numbertheory-629.mm	9
metamath/valid/mathd-numbertheory-64.mm	10
metamath/valid/mathd-numbertheory-640.mm	7
metamath/valid/mathd-numbertheory-668.mm	16
metamath/valid/mathd-numbertheory-690.mm	12
metamath/valid/mathd-numbertheory-709.mm	10
metamath/valid/mathd-numbertheory-739.mm	7
metamath/valid/mathd-numbertheory-780.mm	13
metamath/valid/mathd-numbertheory-81.mm	7
metamath/valid/mathd-numbertheory-84.mm	7
metamath/valid/mathd-numbertheory-92.mm	9
metamath/valid/mathd-numbertheory-961.mm	7
metamath/valid/numbertheory-2dvd4expn.mm	9
metamath/valid/numbertheory-aneqprodakp4-anmsqrtanp1eq2.mm	11
metamath/valid/numbertheory-nckeqnm1ckpnm1ckm1.mm	10
metamath/valid/numbertheory-prmdvsneqnsqmodpeq0.mm	76
metamath/valid/numbertheory-sqmod3in01d.mm	8
metamath/valid/numbertheory-sqmod4in01d.mm	37
metamath/valid/numbertheory-sumkmulnckeqnmul2pownm1.mm	8
metamath/valid/numbertheory-xsqpysqintdenomeq.mm	46