with prfs w/o proofs prf % file 2638588696 1829564816 .3066 <- total 13744040 12881840 .0627 Mathlib/LinearAlgebra/TensorProduct.olean 13064600 12263384 .0613 Mathlib/RingTheory/TensorProduct.olean 11742536 11426464 .0269 Mathlib/Tactic/Ring/Basic.olean 10997048 9833712 .1057 Mathlib/Analysis/NormedSpace/Multilinear.olean 11203032 9412040 .1598 Mathlib/Analysis/NormedSpace/OperatorNorm.olean 9131928 8843960 .0315 Mathlib/Algebra/Lie/BaseChange.olean 8939736 8604072 .0375 Mathlib/Tactic/NormNum/Basic.olean 8547120 8378648 .0197 Mathlib/CategoryTheory/Limits/Cones.olean 8488096 8100696 .0456 Mathlib/Algebra/Lie/Classical.olean 9000344 7827536 .1303 Mathlib/Algebra/Module/LocalizedModule.olean 8764496 7699544 .1215 Mathlib/Topology/Algebra/Module/Basic.olean 7642368 7639832 .0003 Mathlib/Tactic/Linarith/Preprocessing.olean 7639864 7078056 .0735 Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.olean 6984672 6776568 .0297 Mathlib/RepresentationTheory/Action.olean 8503752 6339272 .2545 Mathlib/GroupTheory/Subgroup/Basic.olean 6628208 6314728 .0472 Mathlib/RingTheory/Subsemiring/Basic.olean 6508648 6256376 .0387 Mathlib/FieldTheory/Subfield.olean 7574456 6029552 .2039 Mathlib/LinearAlgebra/Basic.olean 6979280 5856144 .1609 Mathlib/Algebra/Lie/Weights.olean 5673824 5625824 .0084 Mathlib/Tactic/ToAdditive.olean 5510776 5495208 .0028 Mathlib/Mathport/Notation.olean 6114552 5364184 .1227 Mathlib/LinearAlgebra/Multilinear/Basic.olean 5484072 5330096 .0280 Mathlib/Tactic/Simps/Basic.olean 6555200 5204800 .2060 Mathlib/FieldTheory/RatFunc.olean 5485064 5083040 .0732 Mathlib/Algebra/Lie/TensorProduct.olean 5514928 5069944 .0806 Mathlib/Algebra/DirectSum/Ring.olean 7282016 5011952 .3117 Mathlib/FieldTheory/Adjoin.olean 5108760 4987160 .0238 Mathlib/LinearAlgebra/DirectSum/TensorProduct.olean 5210544 4879360 .0635 Mathlib/Topology/ContinuousFunction/Algebra.olean 8378040 4844672 .4217 Mathlib/Computability/TuringMachine.olean 5080768 4831040 .0491 Mathlib/AlgebraicTopology/SimplicialObject.olean 4778984 4715192 .0133 Mathlib/Tactic/Polyrith.olean 5095176 4692600 .0790 Mathlib/RingTheory/Subring/Basic.olean 5221712 4631624 .1130 Mathlib/Algebra/Quaternion.olean 5361952 4489056 .1627 Mathlib/CategoryTheory/Limits/Shapes/Biproducts.olean 6058904 4416856 .2710 Mathlib/GroupTheory/MonoidLocalization.olean 5935776 4336160 .2694 Mathlib/LinearAlgebra/Matrix/ToLin.olean 4681776 4316768 .0779 Mathlib/LinearAlgebra/PiTensorProduct.olean 6782072 4300272 .3659 Mathlib/LinearAlgebra/Dual.olean 4296632 4265944 .0071 Mathlib/Tactic/Positivity/Basic.olean 4319952 4241704 .0181 Mathlib/Tactic/Congr!.olean 4465240 4134328 .0741 Mathlib/CategoryTheory/Monoidal/Mon_.olean 4671424 4100096 .1223 Mathlib/Algebra/Algebra/Subalgebra/Basic.olean 6047056 4059568 .3286 Mathlib/Data/Dfinsupp/Basic.olean 4181544 4046240 .0323 Mathlib/Tactic/NormNum/Core.olean 4360200 3922032 .1004 Mathlib/Algebra/RingQuot.olean 4473512 3840912 .1414 Mathlib/GroupTheory/Submonoid/Operations.olean 4190752 3784480 .0969 Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.olean 3671816 3670208 .0004 Mathlib/LinearAlgebra/BilinearForm/TensorProduct.olean 4800168 3642320 .2412 Mathlib/LinearAlgebra/Alternating.olean 3705608 3568672 .0369 Mathlib/CategoryTheory/Limits/Opposites.olean 4317720 3566776 .1739 Mathlib/Algebra/MonoidAlgebra/Basic.olean 3488816 3463792 .0071 Mathlib/CategoryTheory/Functor/Currying.olean 4923104 3453560 .2984 Mathlib/AlgebraicGeometry/StructureSheaf.olean 4049224 3451664 .1475 Mathlib/Algebra/Lie/Basic.olean 3885200 3439216 .1147 Mathlib/CategoryTheory/Sites/Sheaf.olean 3493088 3385312 .0308 Mathlib/Algebra/Star/StarAlgHom.olean 5943664 3380544 .4312 Mathlib/Analysis/InnerProductSpace/Basic.olean 4454856 3355976 .2466 Mathlib/RingTheory/Localization/Basic.olean 3468808 3282312 .0537 Mathlib/Analysis/NormedSpace/Star/Multiplier.olean 4191624 3218392 .2321 Mathlib/Data/Matrix/Basic.olean 3581416 3213784 .1026 Mathlib/CategoryTheory/Limits/IsLimit.olean 4828744 3210624 .3351 Mathlib/RingTheory/HahnSeries.olean 3452544 3205992 .0714 Mathlib/FieldTheory/PerfectClosure.olean 3215128 3200440 .0045 Mathlib/Logic/Equiv/TransferInstance.olean 3269560 3199752 .0213 Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.olean 3320240 3187648 .0399 Mathlib/Tactic/Abel.olean 3476808 3161432 .0907 Mathlib/Algebra/Module/LinearMap.olean 3473888 3156064 .0914 Mathlib/Analysis/SchwartzSpace.olean 3240608 3134088 .0328 Mathlib/CategoryTheory/StructuredArrow.olean 3475432 3094752 .1095 Mathlib/GroupTheory/Congruence.olean 3075560 3055536 .0065 Mathlib/Tactic/RelCongr/Core.olean 3626832 3052584 .1583 Mathlib/ModelTheory/Syntax.olean 3329160 3038520 .0873 Mathlib/Analysis/NormedSpace/LinearIsometry.olean 3045328 3030400 .0049 Mathlib/CategoryTheory/Adjunction/Evaluation.olean 5242176 3014000 .4250 Mathlib/Computability/TMToPartrec.olean 6264328 3010408 .5194 Mathlib/Data/List/Basic.olean 5023992 3002336 .4024 Mathlib/LinearAlgebra/Matrix/SesquilinearForm.olean 2989216 2973600 .0052 Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.olean 2999008 2963472 .0118 Mathlib/CategoryTheory/Yoneda.olean 2966480 2960384 .0020 Mathlib/CategoryTheory/Preadditive/EilenbergMoore.olean 3614088 2957456 .1816 Mathlib/LinearAlgebra/Dfinsupp.olean 2929920 2923824 .0020 Mathlib/CategoryTheory/Preadditive/EndoFunctor.olean 3251808 2912200 .1044 Mathlib/RingTheory/Ideal/QuotientOperations.olean 2967800 2902696 .0219 Mathlib/Tactic/Positivity/Core.olean 3431016 2894544 .1563 Mathlib/Topology/ContinuousFunction/Bounded.olean 4205248 2889368 .3129 Mathlib/Analysis/Normed/Group/Basic.olean 4028128 2877616 .2856 Mathlib/LinearAlgebra/LinearPMap.olean 2886504 2870568 .0055 Mathlib/Tactic/GCongr/Core.olean 2993776 2862848 .0437 Mathlib/Algebra/Lie/SkewAdjoint.olean 3136128 2857536 .0888 Mathlib/LinearAlgebra/Pi.olean 3167696 2856624 .0982 Mathlib/Algebra/Free.olean 4455088 2849632 .3603 Mathlib/Order/Filter/Basic.olean 3626896 2831760 .2192 Mathlib/NumberTheory/Zsqrtd/Basic.olean 3054960 2828056 .0742 Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.olean 3947760 2772256 .2977 Mathlib/LinearAlgebra/Finsupp.olean 3721744 2715656 .2703 Mathlib/LinearAlgebra/Prod.olean 3173448 2706984 .1469 Mathlib/LinearAlgebra/AffineSpace/AffineMap.olean 2822432 2668768 .0544 Mathlib/Topology/ContinuousFunction/ZeroAtInfty.olean 2686552 2665888 .0076 Mathlib/Topology/LocallyConstant/Algebra.olean 2806640 2661344 .0517 Mathlib/CategoryTheory/Comma.olean 2836168 2645904 .0670 Mathlib/Algebra/FreeAlgebra.olean 4798304 2641872 .4494 Mathlib/LinearAlgebra/Basis.olean 3754528 2639928 .2968 Mathlib/AlgebraicGeometry/OpenImmersion/Basic.olean 2945848 2636416 .1050 Mathlib/GroupTheory/QuotientGroup.olean 2911512 2635640 .0947 Mathlib/Order/Hom/Lattice.olean 3903248 2616424 .3296 Mathlib/LinearAlgebra/BilinearForm.olean 2629000 2607208 .0082 Mathlib/CategoryTheory/Adjunction/Limits.olean 2939208 2598600 .1158 Mathlib/CategoryTheory/Limits/Shapes/Kernels.olean 3033656 2595936 .1442 Mathlib/Logic/Equiv/Basic.olean 2575408 2562032 .0051 Mathlib/CategoryTheory/Subobject/MonoOver.olean 4096496 2558584 .3754 Mathlib/MeasureTheory/Function/LpSpace.olean 3682072 2558448 .3051 Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.olean 3109128 2540176 .1829 Mathlib/Algebra/Homology/Homotopy.olean 3609136 2532384 .2983 Mathlib/GroupTheory/FreeGroup.olean 3558160 2530488 .2888 Mathlib/GroupTheory/FreeProduct.olean 2530680 2529720 .0003 Mathlib/CategoryTheory/Limits/Preserves/Basic.olean 2532032 2506368 .0101 Mathlib/Data/Ordmap/Ordnode.olean 4637040 2487880 .4634 Mathlib/Algebra/DirectLimit.olean 2530736 2484888 .0181 Mathlib/CategoryTheory/Limits/ConeCategory.olean 2543968 2479064 .0255 Mathlib/Topology/Algebra/Module/Multilinear.olean 3097008 2477376 .2000 Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.olean 4701488 2473024 .4739 Mathlib/RingTheory/PowerSeries/Basic.olean 3144376 2455408 .2191 Mathlib/CategoryTheory/Preadditive/Biproducts.olean 2521000 2445112 .0301 Mathlib/Algebra/Group/Opposite.olean 2537576 2438328 .0391 Mathlib/CategoryTheory/Monoidal/Center.olean 2682816 2428120 .0949 Mathlib/CategoryTheory/Bicategory/Free.olean 2813224 2424880 .1380 Mathlib/Algebra/Star/Subalgebra.olean 2740000 2418600 .1172 Mathlib/CategoryTheory/Limits/Shapes/Equalizers.olean 3003728 2417688 .1951 Mathlib/NumberTheory/Dioph.olean 2423488 2395160 .0116 Mathlib/Algebra/Order/Nonneg/Ring.olean 4765632 2394488 .4975 Mathlib/RingTheory/Ideal/Operations.olean 2406184 2377544 .0119 Mathlib/CategoryTheory/Limits/KanExtension.olean 2425200 2371232 .0222 Mathlib/Algebra/Homology/Single.olean 2455088 2360744 .0384 Mathlib/Algebra/Homology/Additive.olean 2822040 2340688 .1705 Mathlib/Algebra/Hom/Group.olean 2655408 2311344 .1295 Mathlib/RingTheory/Ideal/Quotient.olean 3710800 2310328 .3774 Mathlib/Topology/MetricSpace/Basic.olean 2384392 2296032 .0370 Mathlib/CategoryTheory/Products/Basic.olean 2294512 2294064 .0001 Mathlib/Tactic/LibrarySearch.olean 2867880 2276856 .2060 Mathlib/CategoryTheory/Shift/Basic.olean 2834976 2274624 .1976 Mathlib/Combinatorics/SimpleGraph/Basic.olean 2909640 2266104 .2211 Mathlib/RingTheory/OreLocalization/Basic.olean 2235824 2235248 .0002 Mathlib/Order/Copy.olean 2622016 2216336 .1547 Mathlib/Algebra/Homology/HomologicalComplex.olean 2382440 2207584 .0733 Mathlib/Algebra/Lie/Subalgebra.olean 2284648 2206632 .0341 Mathlib/Tactic/IntervalCases.olean 2207944 2198112 .0044 Mathlib/Tactic/PushNeg.olean 2698400 2195520 .1863 Mathlib/SetTheory/Game/PGame.olean 2461176 2194704 .1082 Mathlib/CategoryTheory/Monad/Basic.olean 2211168 2186736 .0110 Mathlib/RingTheory/Congruence.olean 2623152 2184720 .1671 Mathlib/CategoryTheory/Equivalence.olean 2440496 2180296 .1066 Mathlib/CategoryTheory/Monoidal/Free/Coherence.olean 2852184 2180064 .2356 Mathlib/Algebra/Lie/Submodule.olean 2267992 2170864 .0428 Mathlib/Tactic/CancelDenoms.olean 2427624 2165792 .1078 Mathlib/Algebra/Module/Equiv.olean 4110768 2165072 .4733 Mathlib/Data/Seq/WSeq.olean 2368904 2162416 .0871 Mathlib/Algebra/Module/GradedModule.olean 2163280 2159192 .0018 Mathlib/Algebra/Category/Ring/Constructions.olean 2905392 2141272 .2630 Mathlib/Data/Finset/Pointwise.olean 2528040 2131008 .1570 Mathlib/CategoryTheory/Bicategory/Functor.olean 2887632 2130040 .2623 Mathlib/Algebra/Category/Mon/FilteredColimits.olean 2340704 2128200 .0907 Mathlib/Topology/Sheaves/Presheaf.olean 2128152 2118112 .0047 Mathlib/Tactic/MkIffOfInductiveProp.olean 4079568 2114968 .4815 Mathlib/Combinatorics/SimpleGraph/Connectivity.olean 2462504 2110136 .1430 Mathlib/Analysis/NormedSpace/AffineIsometry.olean 2363464 2107504 .1082 Mathlib/CategoryTheory/Elements.olean 2121008 2096152 .0117 Mathlib/CategoryTheory/Monoidal/CommMon_.olean 3984272 2093616 .4745 Mathlib/RingTheory/FractionalIdeal.olean 2919824 2083424 .2864 Mathlib/LinearAlgebra/QuadraticForm/Basic.olean 2328624 2082944 .1055 Mathlib/CategoryTheory/Monoidal/Functor.olean 2444152 2079520 .1491 Mathlib/RingTheory/Valuation/ValuationRing.olean 2995968 2079512 .3058 Mathlib/Analysis/InnerProductSpace/PiL2.olean 2305688 2070176 .1021 Mathlib/Analysis/Normed/Field/Basic.olean 2366072 2054760 .1315 Mathlib/GroupTheory/Coset.olean 3544256 2052560 .4208 Mathlib/Data/Multiset/Basic.olean 2203560 2046408 .0713 Mathlib/Algebra/Group/Prod.olean 2754632 2046104 .2572 Mathlib/RingTheory/AdjoinRoot.olean 2044280 2044280 .0000 Mathlib/Tactic/HelpCmd.olean 2071952 2040416 .0152 Mathlib/CategoryTheory/Whiskering.olean 2196472 2028784 .0763 Mathlib/CategoryTheory/Endofunctor/Algebra.olean 2430776 2022176 .1680 Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.olean 2026672 2016280 .0051 Mathlib/Tactic/Tauto.olean 2365480 2016016 .1477 Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.olean 2903624 2012024 .3070 Mathlib/Analysis/NormedSpace/lpSpace.olean 3199832 2011336 .3714 Mathlib/FieldTheory/Normal.olean 2211064 2010920 .0905 Mathlib/CategoryTheory/Preadditive/Mat.olean 2141240 2006712 .0628 Mathlib/CategoryTheory/Limits/Shapes/Terminal.olean 1998328 1998328 .0000 Mathlib/Tactic/DeriveToExpr.olean 4226720 1983112 .5308 Mathlib/MeasureTheory/Measure/MeasureSpace.olean 2012816 1982536 .0150 Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.olean 2369024 1979144 .1645 Mathlib/LinearAlgebra/Quotient.olean 2054680 1976696 .0379 Mathlib/Tactic/Sat/FromLRAT.olean 2176712 1969392 .0952 Mathlib/Algebra/TrivSqZeroExt.olean 1998104 1965880 .0161 Mathlib/Algebra/Group/InjSurj.olean 1998296 1960456 .0189 Mathlib/Algebra/Hom/GroupInstances.olean 2676576 1951264 .2709 Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.olean 1949688 1949688 .0000 Mathlib/Tactic/NormCast/Tactic.olean 2984616 1934368 .3518 Mathlib/Topology/UniformSpace/Basic.olean 2204776 1933480 .1230 Mathlib/MeasureTheory/Function/AEEqFun.olean 1969520 1926336 .0219 Mathlib/Tactic/Ring/RingNF.olean 2492672 1922800 .2286 Mathlib/Topology/Algebra/ContinuousMonoidHom.olean 1956064 1919864 .0185 Mathlib/Tactic/SolveByElim.olean 3220632 1918408 .4043 Mathlib/Topology/Algebra/Group/Basic.olean 1967280 1912768 .0277 Mathlib/CategoryTheory/Monoidal/Free/Basic.olean 1943080 1912368 .0158 Mathlib/AlgebraicTopology/CechNerve.olean 2590176 1907768 .2634 Mathlib/RingTheory/Noetherian.olean 3183920 1907208 .4009 Mathlib/Data/Num/Lemmas.olean 2017144 1903672 .0562 Mathlib/CategoryTheory/Limits/FunctorCategory.olean 1988464 1903248 .0428 Mathlib/Algebra/Algebra/Unitization.olean 2117632 1902944 .1013 Mathlib/Algebra/Algebra/Equiv.olean 1984528 1888616 .0483 Mathlib/Algebra/Module/Submodule/Basic.olean 2445648 1884664 .2293 Mathlib/Algebra/Homology/ShortComplex/LeftHomology.olean 1942904 1880696 .0320 Mathlib/CategoryTheory/Opposites.olean 2040088 1858520 .0890 Mathlib/CategoryTheory/Monad/Algebra.olean 2500800 1858104 .2569 Mathlib/LinearAlgebra/TensorPower.olean 2044544 1852176 .0940 Mathlib/RingTheory/Derivation/Basic.olean 2037208 1849752 .0920 Mathlib/RingTheory/GradedAlgebra/Basic.olean 2246704 1837560 .1821 Mathlib/CategoryTheory/Subobject/Basic.olean 2027640 1823240 .1008 Mathlib/RingTheory/Ideal/Cotangent.olean 1858624 1818880 .0213 Mathlib/CategoryTheory/Pi/Basic.olean 2390104 1818184 .2392 Mathlib/MeasureTheory/MeasurableSpace.olean 1999360 1816112 .0916 Mathlib/Order/Hom/Basic.olean 1819504 1810280 .0050 Mathlib/CategoryTheory/Monad/Adjunction.olean 1999848 1809256 .0953 Mathlib/CategoryTheory/Idempotents/FunctorExtension.olean 2492240 1807136 .2748 Mathlib/LinearAlgebra/Contraction.olean 2196520 1798696 .1811 Mathlib/Algebra/Group/Defs.olean 3606048 1798232 .5013 Mathlib/MeasureTheory/Integral/Bochner.olean 3028928 1795712 .4071 Mathlib/Data/Finset/Basic.olean 1872032 1788264 .0447 Mathlib/CategoryTheory/Limits/Constructions/Over/Products.olean 1861832 1787872 .0397 Mathlib/Algebra/Homology/Augment.olean 2497392 1786392 .2846 Mathlib/Topology/Homotopy/HomotopyGroup.olean 3386608 1785824 .4726 Mathlib/RingTheory/DedekindDomain/Ideal.olean 2374520 1783760 .2487 Mathlib/CategoryTheory/Limits/HasLimits.olean 1798648 1777760 .0116 Mathlib/Tactic/ProxyType.olean 2465696 1771408 .2815 Mathlib/MeasureTheory/Function/SimpleFunc.olean 2475336 1767408 .2859 Mathlib/Combinatorics/SimpleGraph/Subgraph.olean 1961384 1761320 .1020 Mathlib/LinearAlgebra/AdicCompletion.olean 1850528 1755856 .0511 Mathlib/CategoryTheory/Over.olean 1750368 1750368 .0000 Mathlib/Tactic/Relation/Trans.olean 2380072 1750032 .2647 Mathlib/Topology/VectorBundle/Basic.olean 1812936 1738232 .0412 Mathlib/CategoryTheory/Monoidal/Mod_.olean 1908944 1737064 .0900 Mathlib/LinearAlgebra/BilinearMap.olean 1799448 1727840 .0397 Mathlib/Data/Sum/Order.olean 1802288 1720664 .0452 Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.olean 1731080 1716464 .0084 Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.olean 2184584 1714920 .2149 Mathlib/Data/Sym/Sym2.olean 2266632 1713032 .2442 Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.olean 1711352 1710056 .0007 Mathlib/CategoryTheory/Linear/FunctorCategory.olean 1983952 1706416 .1398 Mathlib/CategoryTheory/Adjunction/Basic.olean 1939408 1705872 .1204 Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.olean 1730600 1703456 .0156 Mathlib/Tactic/Rewrites.olean 2136760 1701200 .2038 Mathlib/Data/List/Forall2.olean 2704088 1695984 .3728 Mathlib/Analysis/NormedSpace/FiniteDimension.olean 1915032 1695256 .1147 Mathlib/RingTheory/NonUnitalSubsemiring/Basic.olean 1819136 1695232 .0681 Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.olean 1820536 1686984 .0733 Mathlib/Order/LocallyFinite.olean 2497944 1685448 .3252 Mathlib/CategoryTheory/Monoidal/Rigid/Basic.olean 2483992 1682520 .3226 Mathlib/MeasureTheory/Function/L1Space.olean 1772216 1664712 .0606 Mathlib/Algebra/Hom/Equiv/Basic.olean 1980584 1663856 .1599 Mathlib/GroupTheory/GroupAction/Defs.olean 1718568 1656696 .0360 Mathlib/Order/Filter/Germ.olean 1707880 1654160 .0314 Mathlib/Algebra/Category/Ring/Colimits.olean 2270208 1651528 .2725 Mathlib/Analysis/NormedSpace/BoundedLinearMaps.olean 2622872 1633472 .3772 Mathlib/Data/Real/ENNReal.olean 1794784 1632640 .0903 Mathlib/Algebra/Order/Interval.olean 1937408 1626160 .1606 Mathlib/CategoryTheory/Limits/Final.olean 1694920 1624864 .0413 Mathlib/Testing/SlimCheck/Testable.olean 1813000 1613688 .1099 Mathlib/GroupTheory/FreeAbelianGroup.olean 1658008 1600392 .0347 Mathlib/Order/Filter/FilterProduct.olean 1593888 1593888 .0000 Mathlib/Tactic/TFAE.olean 1692008 1593256 .0583 Mathlib/CategoryTheory/Limits/Creates.olean 2178464 1592792 .2688 Mathlib/Order/CompleteLattice.olean 1800552 1590000 .1169 Mathlib/LinearAlgebra/FinsuppVectorSpace.olean 1705776 1576376 .0758 Mathlib/Analysis/Normed/Group/Seminorm.olean 1643136 1574408 .0418 Mathlib/CategoryTheory/DifferentialObject.olean 2291072 1573640 .3131 Mathlib/Data/Real/CauSeq.olean 2312664 1570864 .3207 Mathlib/MeasureTheory/Measure/VectorMeasure.olean 2393848 1570208 .3440 Mathlib/Analysis/Seminorm.olean 1618184 1567024 .0316 Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.olean 1932584 1536152 .2051 Mathlib/Algebra/Group/Pi.olean 2228904 1534664 .3114 Mathlib/RingTheory/IsAdjoinRoot.olean 1925640 1532832 .2039 Mathlib/RepresentationTheory/Basic.olean 1843624 1532432 .1687 Mathlib/Order/Heyting/Basic.olean 1658048 1530584 .0768 Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.olean 2603432 1530296 .4122 Mathlib/LinearAlgebra/Matrix/BilinearForm.olean 5111040 1529816 .7006 Mathlib/ModelTheory/Semantics.olean 2030312 1529496 .2466 Mathlib/Order/Basic.olean 2451104 1528136 .3765 Mathlib/NumberTheory/ArithmeticFunction.olean 1695960 1524936 .1008 Mathlib/AlgebraicGeometry/PresheafedSpace.olean 1797728 1524736 .1518 Mathlib/Analysis/Normed/Group/Hom.olean 1615904 1523240 .0573 Mathlib/Data/Analysis/Filter.olean 1941440 1515616 .2193 Mathlib/Algebra/GCDMonoid/Basic.olean 1597928 1514424 .0522 Mathlib/CategoryTheory/WithTerminal.olean 7210760 1514048 .7900 Mathlib/Analysis/Calculus/ContDiff.olean 1632256 1513272 .0728 Mathlib/Algebra/Hom/NonUnitalAlg.olean 1673624 1512856 .0960 Mathlib/Order/Hom/CompleteLattice.olean 1561072 1505336 .0357 Mathlib/Algebra/Category/ModuleCat/Colimits.olean 1813848 1505192 .1701 Mathlib/Data/Fintype/Basic.olean 1924736 1499768 .2207 Mathlib/CategoryTheory/Bicategory/Coherence.olean 1718144 1498192 .1280 Mathlib/Algebra/Lie/Abelian.olean 2401112 1490848 .3791 Mathlib/Data/Finsupp/Basic.olean 1488464 1488112 .0002 Mathlib/LinearAlgebra/TensorAlgebra/Grading.olean 1504264 1488096 .0107 Mathlib/CategoryTheory/Limits/Bicones.olean 1778664 1483424 .1659 Mathlib/CategoryTheory/Monoidal/Category.olean 1788000 1473352 .1759 Mathlib/GroupTheory/Subsemigroup/Operations.olean 2142496 1468936 .3143 Mathlib/RingTheory/Perfection.olean 1687552 1468328 .1299 Mathlib/Algebra/Order/Hom/Monoid.olean 1477496 1466176 .0076 Mathlib/Tactic/CategoryTheory/Coherence.olean 1584856 1461696 .0777 Mathlib/Algebra/Hom/GroupAction.olean 1456848 1456848 .0000 Mathlib/Tactic/Linarith/Frontend.olean 1554032 1456448 .0627 Mathlib/Algebra/Algebra/Hom.olean 2213216 1450728 .3445 Mathlib/Analysis/InnerProductSpace/l2Space.olean 5196040 1448488 .7212 Mathlib/Data/Ordmap/Ordset.olean 3026424 1448184 .5214 Mathlib/NumberTheory/RamificationInertia.olean 1443720 1441536 .0015 Mathlib/Util/CompileInductive.olean 1491160 1439408 .0347 Mathlib/Util/Export.olean 3263536 1431656 .5613 Mathlib/Algebra/BigOperators/Basic.olean 1570544 1428808 .0902 Mathlib/Order/Heyting/Hom.olean 1434456 1427408 .0049 Mathlib/CategoryTheory/Monoidal/Discrete.olean 1716496 1421864 .1716 Mathlib/Geometry/Manifold/ChartedSpace.olean 1635328 1421112 .1309 Mathlib/Algebra/Quandle.olean 1425032 1420416 .0032 Mathlib/CategoryTheory/Linear/Yoneda.olean 1964392 1417128 .2785 Mathlib/RingTheory/WittVector/Basic.olean 1425800 1416008 .0068 Mathlib/Algebra/Group/ULift.olean 1446536 1412408 .0235 Mathlib/CategoryTheory/Sigma/Basic.olean 1527048 1410736 .0761 Mathlib/CategoryTheory/Enriched/Basic.olean 1900184 1409344 .2583 Mathlib/CategoryTheory/Subobject/Lattice.olean 1883992 1406392 .2535 Mathlib/Order/Filter/Pointwise.olean 1466400 1399664 .0455 Mathlib/Tactic/FBinop.olean 1397120 1397120 .0000 Mathlib/Tactic/Basic.olean 1396392 1396392 .0000 Mathlib/Tactic/ScopedNS.olean 1660536 1395760 .1594 Mathlib/ModelTheory/Basic.olean 1939360 1391480 .2825 Mathlib/SetTheory/Ordinal/Basic.olean 1682200 1382600 .1781 Mathlib/CategoryTheory/Bicategory/NaturalTransformation.olean 2564640 1374696 .4639 Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.olean 1838440 1372192 .2536 Mathlib/SetTheory/ZFC/Basic.olean 1470672 1371544 .0674 Mathlib/Topology/Algebra/Nonarchimedean/Bases.olean 1456296 1371504 .0582 Mathlib/Data/Dfinsupp/Lex.olean 2092024 1365624 .3472 Mathlib/RingTheory/RootsOfUnity/Basic.olean 1451016 1362312 .0611 Mathlib/Algebra/Lie/Free.olean 2529416 1359016 .4627 Mathlib/LinearAlgebra/Determinant.olean 1356520 1355608 .0006 Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.olean 1662264 1354896 .1849 Mathlib/Analysis/NormedSpace/Basic.olean 1926208 1354728 .2966 Mathlib/NumberTheory/KummerDedekind.olean 1405936 1354568 .0365 Mathlib/Algebra/Homology/Opposite.olean 2336416 1350992 .4217 Mathlib/SetTheory/Cardinal/Basic.olean 2370024 1347688 .4313 Mathlib/Data/Fin/Basic.olean 1361328 1347104 .0104 Mathlib/CategoryTheory/Limits/Comma.olean 1480408 1343232 .0926 Mathlib/Logic/Equiv/Defs.olean 1382640 1343208 .0285 Mathlib/Algebra/Hom/Centroid.olean 3574344 1337832 .6257 Mathlib/CategoryTheory/Monoidal/Braided.olean 1950592 1336776 .3146 Mathlib/CategoryTheory/Sites/Sieves.olean 1434976 1334824 .0697 Mathlib/Algebra/Star/SelfAdjoint.olean 2106344 1318320 .3741 Mathlib/Algebra/Algebra/Operations.olean 1387320 1316392 .0511 Mathlib/Tactic/Linarith/Datatypes.olean 1319696 1316264 .0026 Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.olean 2773504 1315856 .5255 Mathlib/Data/MvPolynomial/Basic.olean 1326888 1307264 .0147 Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.olean 3160080 1307072 .5863 Mathlib/Analysis/InnerProductSpace/Projection.olean 1299864 1299864 .0000 Mathlib/Lean/Meta/Simp.olean 1491264 1296488 .1306 Mathlib/Logic/Equiv/Set.olean 1646488 1291216 .2157 Mathlib/CategoryTheory/Monoidal/End.olean 2530040 1291072 .4897 Mathlib/RingTheory/IsTensorProduct.olean 1719320 1290664 .2493 Mathlib/Data/Complex/Basic.olean 1399192 1290552 .0776 Mathlib/Order/Hom/Bounded.olean 1456136 1289208 .1146 Mathlib/GroupTheory/SpecificGroups/Quaternion.olean 1879288 1281472 .3181 Mathlib/Data/Seq/Computation.olean 1283824 1278848 .0038 Mathlib/Tactic/Choose.olean 1278320 1278320 .0000 Mathlib/Tactic/Linarith/Parsing.olean 2347096 1277512 .4557 Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.olean 1538888 1277160 .1700 Mathlib/Topology/Homotopy/Basic.olean 3008808 1276320 .5758 Mathlib/RingTheory/Polynomial/Basic.olean 1931912 1275200 .3399 Mathlib/Analysis/Convex/Cone/Basic.olean 1915832 1270656 .3367 Mathlib/Data/Matrix/Kronecker.olean 1504776 1270352 .1557 Mathlib/CategoryTheory/Limits/Shapes/Types.olean 1456736 1269976 .1282 Mathlib/CategoryTheory/Limits/Presheaf.olean 1650512 1269056 .2311 Mathlib/Algebra/Module/Injective.olean 1933376 1268088 .3441 Mathlib/Algebra/Order/Group/Defs.olean 1264824 1264824 .0000 Mathlib/Algebra/Ring/InjSurj.olean 1267024 1260304 .0053 Mathlib/Algebra/Homology/Flip.olean 1604376 1259384 .2150 Mathlib/Algebra/Order/Ring/Defs.olean 1472192 1258664 .1450 Mathlib/Algebra/Hom/Freiman.olean 2230448 1256776 .4365 Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.olean 1302568 1250320 .0401 Mathlib/Topology/Algebra/UniformRing.olean 1250096 1250096 .0000 Mathlib/Topology/Category/TopCat/Limits/Basic.olean 1249824 1249824 .0000 Mathlib/Tactic/IrreducibleDef.olean 1355840 1249520 .0784 Mathlib/CategoryTheory/Abelian/InjectiveResolution.olean 1313160 1247856 .0497 Mathlib/Topology/Algebra/ContinuousAffineMap.olean 1949256 1243264 .3621 Mathlib/CategoryTheory/Sites/Grothendieck.olean 1452888 1243248 .1442 Mathlib/CategoryTheory/Limits/Fubini.olean 2547360 1242216 .5123 Mathlib/Analysis/Asymptotics/Asymptotics.olean 1246976 1239488 .0060 Mathlib/CategoryTheory/Adjunction/Whiskering.olean 2582512 1238272 .5205 Mathlib/Computability/PartrecCode.olean 2135016 1234952 .4215 Mathlib/RingTheory/PowerBasis.olean 1430392 1231536 .1390 Mathlib/AlgebraicTopology/ExtraDegeneracy.olean 1228776 1228776 .0000 Mathlib/CategoryTheory/Preadditive/LeftExact.olean 1277768 1228696 .0384 Mathlib/Algebra/Lie/Matrix.olean 1260184 1222856 .0296 Mathlib/Tactic/LinearCombination.olean 1248128 1221160 .0216 Mathlib/CategoryTheory/Monoidal/Transport.olean 1241688 1218960 .0183 Mathlib/CategoryTheory/Preadditive/FunctorCategory.olean 1370656 1218424 .1110 Mathlib/Order/RelIso/Basic.olean 1405904 1214504 .1361 Mathlib/Topology/ContinuousFunction/Compact.olean 2744568 1211368 .5586 Mathlib/Topology/Order/Basic.olean 1492976 1211024 .1888 Mathlib/LinearAlgebra/QuotientPi.olean 1532560 1210144 .2103 Mathlib/Algebra/DirectSum/Module.olean 1378880 1209504 .1228 Mathlib/Data/Real/CauSeqCompletion.olean 1464592 1207224 .1757 Mathlib/Data/TypeVec.olean 1593680 1207120 .2425 Mathlib/Order/ConditionallyCompleteLattice/Basic.olean 1972208 1206688 .3881 Mathlib/Algebra/Module/Torsion.olean 1576736 1204760 .2359 Mathlib/Logic/Equiv/LocalEquiv.olean 1316576 1202560 .0866 Mathlib/CategoryTheory/Abelian/Basic.olean 1261024 1201160 .0474 Mathlib/CategoryTheory/Skeletal.olean 3633864 1197312 .6705 Mathlib/SetTheory/Ordinal/Arithmetic.olean 1299408 1196720 .0790 Mathlib/LinearAlgebra/InvariantBasisNumber.olean 3272480 1192480 .6356 Mathlib/MeasureTheory/Integral/SetToL1.olean 1315848 1192064 .0940 Mathlib/Topology/Homotopy/HSpaces.olean 1470872 1190848 .1903 Mathlib/Order/WithBot.olean 1194472 1189984 .0037 Mathlib/Algebra/Category/ModuleCat/Limits.olean 1199832 1189344 .0087 Mathlib/Tactic/CategoryTheory/BicategoryCoherence.olean 1362360 1188424 .1276 Mathlib/Analysis/NormedSpace/ContinuousAffineMap.olean 1277384 1186888 .0708 Mathlib/Algebra/DirectSum/Basic.olean 1814840 1184360 .3474 Mathlib/CategoryTheory/Groupoid/Subgroupoid.olean 1295472 1182592 .0871 Mathlib/Data/FinEnum.olean 1581568 1182056 .2526 Mathlib/CategoryTheory/Adjunction/Opposites.olean 1214624 1180008 .0284 Mathlib/CategoryTheory/Idempotents/HomologicalComplex.olean 1207200 1179192 .0232 Mathlib/CategoryTheory/DiscreteCategory.olean 1634840 1176000 .2806 Mathlib/Analysis/NormedSpace/PiLp.olean 1494744 1171536 .2162 Mathlib/Topology/UniformSpace/UniformConvergenceTopology.olean 1915392 1170544 .3888 Mathlib/Data/Seq/Seq.olean 3186808 1170488 .6327 Mathlib/GroupTheory/Perm/Cycle/Basic.olean 1405392 1169776 .1676 Mathlib/Algebra/Homology/ShortComplex/Basic.olean 1199304 1166168 .0276 Mathlib/Algebra/Symmetrized.olean 2018640 1164400 .4231 Mathlib/Analysis/InnerProductSpace/Adjoint.olean 1449856 1163416 .1975 Mathlib/Algebra/Algebra/Basic.olean 1320776 1162112 .1201 Mathlib/Algebra/Hom/Ring.olean 1161384 1161384 .0000 Mathlib/Lean/Expr/Basic.olean 1357936 1154824 .1495 Mathlib/ModelTheory/Substructures.olean 1500808 1154504 .2307 Mathlib/Algebra/DirectSum/Internal.olean 1629424 1153936 .2918 Mathlib/RingTheory/Valuation/Basic.olean 1155176 1152352 .0024 Mathlib/Algebra/Ring/Opposite.olean 1155256 1151736 .0030 Mathlib/Tactic/CategoryTheory/Elementwise.olean 1175752 1150856 .0211 Mathlib/CategoryTheory/GradedObject.olean 1894072 1150472 .3925 Mathlib/CategoryTheory/Sites/SheafOfTypes.olean 1150056 1146792 .0028 Mathlib/Tactic/Elementwise.olean 3461944 1139792 .6707 Mathlib/Analysis/Analytic/Composition.olean 1642176 1139312 .3062 Mathlib/Data/IsROrC/Basic.olean 1189120 1136104 .0445 Mathlib/Data/ListM/Basic.olean 2095744 1135760 .4580 Mathlib/Data/Set/Lattice.olean 2001184 1134696 .4329 Mathlib/Analysis/NormedSpace/Spectrum.olean 1415336 1132872 .1995 Mathlib/Order/Partition/Finpartition.olean 1257232 1124872 .1052 Mathlib/Algebra/Ring/Equiv.olean 2920104 1124040 .6150 Mathlib/MeasureTheory/Integral/Lebesgue.olean 1493640 1123744 .2476 Mathlib/CategoryTheory/Limits/Shapes/Images.olean 1122648 1122648 .0000 Mathlib/Algebra/Category/Ring/Limits.olean 1142008 1121968 .0175 Mathlib/CategoryTheory/Sums/Basic.olean 1748864 1121496 .3587 Mathlib/Data/Set/Finite.olean 3191296 1120536 .6488 Mathlib/Analysis/Analytic/Basic.olean 1163384 1120440 .0369 Mathlib/Algebra/Category/GroupCat/Colimits.olean 2784544 1120104 .5977 Mathlib/RingTheory/UniqueFactorizationDomain.olean 1543024 1118408 .2751 Mathlib/Topology/FiberBundle/Basic.olean 1389624 1117480 .1958 Mathlib/Data/Complex/Module.olean 1135560 1115688 .0174 Mathlib/Data/UInt.olean 1805792 1115080 .3824 Mathlib/Topology/Basic.olean 1420752 1108592 .2197 Mathlib/SetTheory/Lists.olean 1117720 1107752 .0089 Mathlib/CategoryTheory/Category/Cat/Limit.olean 2116240 1105384 .4776 Mathlib/MeasureTheory/Measure/OuterMeasure.olean 2033904 1103136 .4576 Mathlib/Data/ZMod/Basic.olean 1166168 1092288 .0633 Mathlib/Algebra/Order/Hom/Ring.olean 1363008 1087720 .2019 Mathlib/Data/Finmap.olean 1736152 1085160 .3749 Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.olean 1257048 1084640 .1371 Mathlib/Topology/FiberBundle/Constructions.olean 1451584 1082856 .2540 Mathlib/Order/Lattice.olean 2461728 1079584 .5614 Mathlib/Topology/SubsetProperties.olean 1257264 1079160 .1416 Mathlib/Algebra/GradedMonoid.olean 1307208 1078808 .1747 Mathlib/Order/GaloisConnection.olean 1636776 1077584 .3416 Mathlib/CategoryTheory/Extensive.olean 1433176 1074776 .2500 Mathlib/Algebra/Category/GroupCat/EpiMono.olean 1155352 1074344 .0701 Mathlib/Topology/Homotopy/Path.olean 1214048 1072488 .1166 Mathlib/CategoryTheory/Grothendieck.olean 1188216 1071912 .0978 Mathlib/Algebra/Category/GroupCat/FilteredColimits.olean 1336992 1068672 .2006 Mathlib/Algebra/Category/ModuleCat/Adjunctions.olean 1086744 1067840 .0173 Mathlib/Order/Category/BddLatCat.olean 1634456 1066992 .3471 Mathlib/Order/UpperLower/Basic.olean 1144152 1066288 .0680 Mathlib/CategoryTheory/Monoidal/NaturalTransformation.olean 1681496 1066176 .3659 Mathlib/Data/Polynomial/Basic.olean 2578384 1065064 .5869 Mathlib/Topology/Algebra/UniformGroup.olean 1732312 1061136 .3874 Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.olean 1369880 1060416 .2259 Mathlib/Topology/Algebra/Module/StrongTopology.olean 1471400 1053728 .2838 Mathlib/FieldTheory/IntermediateField.olean 1492848 1053024 .2946 Mathlib/Algebra/Module/Basic.olean 3565856 1052048 .7049 Mathlib/Analysis/Calculus/ContDiffDef.olean 1322616 1049160 .2067 Mathlib/MeasureTheory/Measure/MeasureSpaceDef.olean 1121536 1048192 .0653 Mathlib/Algebra/Lie/DirectSum.olean 2013904 1047768 .4797 Mathlib/ModelTheory/Encoding.olean 1044064 1044064 .0000 Mathlib/Mathport/Syntax.olean 3076992 1043648 .6608 Mathlib/LinearAlgebra/FreeModule/PID.olean 1215952 1043040 .1422 Mathlib/Topology/VectorBundle/Constructions.olean 1779432 1039080 .4160 Mathlib/Data/Set/Basic.olean 2573088 1035752 .5974 Mathlib/LinearAlgebra/AffineSpace/Combination.olean 1487248 1035736 .3035 Mathlib/Topology/Instances/AddCircle.olean 1714888 1033912 .3970 Mathlib/AlgebraicGeometry/Spec.olean 1376752 1032720 .2498 Mathlib/Topology/FiberBundle/Trivialization.olean 1032144 1032144 .0000 Mathlib/Lean/Meta.olean 1083448 1030528 .0488 Mathlib/Algebra/Order/Kleene.olean 1035208 1027112 .0078 Mathlib/CategoryTheory/Monad/Products.olean 1154528 1026760 .1106 Mathlib/Topology/Homeomorph.olean 2244680 1024712 .5434 Mathlib/Topology/Sheaves/Stalks.olean 1023240 1023240 .0000 Mathlib/Tactic/Relation/Symm.olean 1575872 1022944 .3508 Mathlib/CategoryTheory/Sites/Plus.olean 1022832 1022832 .0000 Mathlib/Tactic/DeriveFintype.olean 1074328 1020952 .0496 Mathlib/Algebra/Category/ModuleCat/Basic.olean 2575584 1020120 .6039 Mathlib/Data/List/Perm.olean 1078152 1018088 .0557 Mathlib/Algebra/Lie/OfAssociative.olean 1237304 1011512 .1824 Mathlib/Analysis/NormedSpace/MStructure.olean 1357744 1011040 .2553 Mathlib/Algebra/Group/Units.olean 1559904 1009456 .3528 Mathlib/Data/MvPolynomial/Equiv.olean 1662784 1009352 .3929 Mathlib/GroupTheory/Sylow.olean 1009000 1009000 .0000 Mathlib/Tactic/Propose.olean 1311472 1007376 .2318 Mathlib/Algebra/MonoidAlgebra/Grading.olean 1288072 1007248 .2180 Mathlib/Order/OmegaCompletePartialOrder.olean 1006984 1006984 .0000 Mathlib/Tactic/ApplyFun.olean 1108056 1005072 .0929 Mathlib/Topology/Algebra/Module/CharacterSpace.olean 1355344 1003696 .2594 Mathlib/GroupTheory/SemidirectProduct.olean 1042304 1003632 .0371 Mathlib/CategoryTheory/Monad/Limits.olean 2077176 1001136 .5180 Mathlib/Topology/Gluing.olean 1023152 1000696 .0219 Mathlib/Algebra/Lie/Quotient.olean 1099568 1000680 .0899 Mathlib/Order/CompleteBooleanAlgebra.olean 1006456 1000472 .0059 Mathlib/Algebra/Category/MonCat/Limits.olean 1036496 993976 .0410 Mathlib/Data/Sigma/Order.olean 998384 990680 .0077 Mathlib/CategoryTheory/Monoidal/Subcategory.olean 1050136 990680 .0566 Mathlib/Topology/Category/TopCat/Opens.olean 1515064 987040 .3485 Mathlib/Topology/MetricSpace/EMetricSpace.olean 1001504 986728 .0147 Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.olean 1025328 986288 .0380 Mathlib/Analysis/BoxIntegral/Partition/Additive.olean 1075192 985272 .0836 Mathlib/Topology/Category/CompHaus/EffectiveEpi.olean 1406080 983504 .3005 Mathlib/Topology/LocalHomeomorph.olean 2045536 983008 .5194 Mathlib/LinearAlgebra/FiniteDimensional.olean 1082080 982344 .0921 Mathlib/CategoryTheory/Idempotents/Karoubi.olean 1028320 980280 .0467 Mathlib/Algebra/Ring/Prod.olean 1125280 976264 .1324 Mathlib/LinearAlgebra/Isomorphisms.olean 1168840 975760 .1651 Mathlib/Topology/Algebra/FilterBasis.olean 978952 975400 .0036 Mathlib/Tactic/Lift.olean 2155800 975296 .5475 Mathlib/Analysis/InnerProductSpace/TwoDim.olean 1362968 975216 .2844 Mathlib/LinearAlgebra/Matrix/NonsingularInverse.olean 2317104 974272 .5795 Mathlib/Topology/Separation.olean 978576 973192 .0055 Mathlib/CategoryTheory/Sums/Associator.olean 1934560 966128 .5005 Mathlib/NumberTheory/PellMatiyasevic.olean 2157768 963088 .5536 Mathlib/GroupTheory/Perm/Sign.olean 1004296 959544 .0445 Mathlib/Tactic/NormNum/GCD.olean 1084696 957192 .1175 Mathlib/CategoryTheory/Sites/LeftExact.olean 1448152 956232 .3396 Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.olean 980424 953200 .0277 Mathlib/Data/List/Defs.olean 1332864 951704 .2859 Mathlib/CategoryTheory/Functor/Flat.olean 952344 951152 .0012 Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.olean 1378416 950168 .3106 Mathlib/Topology/MetricSpace/Gluing.olean 949472 949472 .0000 Mathlib/Data/PSigma/Order.olean 2238984 947144 .5769 Mathlib/CategoryTheory/Sites/Sheafification.olean 1773240 945040 .4670 Mathlib/Data/List/Cycle.olean 1243784 943096 .2417 Mathlib/LinearAlgebra/TensorAlgebra/Basic.olean 1533408 942456 .3853 Mathlib/Data/Finsupp/Defs.olean 1135728 941120 .1713 Mathlib/CategoryTheory/Adjunction/Mates.olean 1071976 939808 .1232 Mathlib/ModelTheory/LanguageMap.olean 1428104 939632 .3420 Mathlib/Algebra/Algebra/Spectrum.olean 1364168 938776 .3118 Mathlib/CategoryTheory/Sites/DenseSubsite.olean 938256 938256 .0000 Mathlib/Tactic/Linarith/Verification.olean 979160 933224 .0469 Mathlib/CategoryTheory/Action.olean 983712 931416 .0531 Mathlib/Data/Quot.olean 929888 929888 .0000 Mathlib/Data/ListM/BestFirst.olean 1229224 928024 .2450 Mathlib/Analysis/NormedSpace/Dual.olean 1498296 926232 .3818 Mathlib/Combinatorics/Composition.olean 1128248 926160 .1791 Mathlib/Data/UnionFind.olean 1082008 923864 .1461 Mathlib/Algebra/Homology/ImageToKernel.olean 1343776 923512 .3127 Mathlib/CategoryTheory/GlueData.olean 1118864 922784 .1752 Mathlib/GroupTheory/Submonoid/Basic.olean 922608 922608 .0000 Mathlib/Tactic/Explode.olean 924024 921120 .0031 Mathlib/Algebra/Order/Nonneg/Field.olean 1237296 910448 .2641 Mathlib/Data/Real/Basic.olean 927264 909112 .0195 Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.olean 1009392 903224 .1051 Mathlib/Algebra/Ring/Defs.olean 1592864 902128 .4336 Mathlib/Algebra/Associated.olean 1452112 899168 .3807 Mathlib/Algebra/BigOperators/Fin.olean 898840 898840 .0000 Mathlib/Tactic/Core.olean 1132352 898784 .2062 Mathlib/Analysis/Calculus/FormalMultilinearSeries.olean 1184568 893456 .2457 Mathlib/CategoryTheory/Abelian/Homology.olean 1284648 892984 .3048 Mathlib/CategoryTheory/Bicategory/Basic.olean 1233440 892976 .2760 Mathlib/Order/SuccPred/Basic.olean 1668872 891032 .4660 Mathlib/FieldTheory/IsAlgClosed/Basic.olean 1456976 890624 .3887 Mathlib/Data/Set/Pointwise/Basic.olean 1081200 889800 .1770 Mathlib/Data/PEquiv.olean 1368320 889112 .3502 Mathlib/Data/Vector/Basic.olean 911632 887464 .0265 Mathlib/RingTheory/Derivation/ToSquareZero.olean 893152 886768 .0071 Mathlib/CategoryTheory/Sites/Limits.olean 1954344 884216 .5475 Mathlib/LinearAlgebra/Span.olean 1415568 882528 .3765 Mathlib/GroupTheory/Perm/Cycle/Concrete.olean 1712904 880960 .4856 Mathlib/RingTheory/Filtration.olean 889376 880704 .0097 Mathlib/CategoryTheory/Limits/Shapes/RegularMono.olean 1177592 879432 .2531 Mathlib/Order/Atoms.olean 976904 878416 .1008 Mathlib/CategoryTheory/Preadditive/Basic.olean 873112 873112 .0000 Mathlib/Algebra/Category/GroupCat/Abelian.olean 925680 871656 .0583 Mathlib/Data/ZMod/Quotient.olean 1024488 871016 .1498 Mathlib/Order/InitialSeg.olean 901776 870464 .0347 Mathlib/Algebra/Lie/CartanMatrix.olean 903328 869072 .0379 Mathlib/Algebra/Category/ModuleCat/Biproducts.olean 1027008 868792 .1540 Mathlib/Algebra/Order/Ring/WithTop.olean 1062792 866976 .1842 Mathlib/CategoryTheory/Functor/FullyFaithful.olean 1014440 866672 .1456 Mathlib/CategoryTheory/Localization/Construction.olean 2204320 860704 .6095 Mathlib/LinearAlgebra/SesquilinearForm.olean 1937352 856344 .5579 Mathlib/MeasureTheory/Integral/IntervalIntegral.olean 865240 854736 .0121 Mathlib/Algebra/Group/TypeTags.olean 1300176 853496 .3435 Mathlib/CategoryTheory/Limits/ConcreteCategory.olean 1060744 851472 .1972 Mathlib/RingTheory/AlgebraTower.olean 1051728 851280 .1905 Mathlib/RingTheory/MatrixAlgebra.olean 850544 849664 .0010 Mathlib/CategoryTheory/Limits/Yoneda.olean 1417208 848272 .4014 Mathlib/Topology/Category/TopCat/Limits/Products.olean 843872 843872 .0000 Mathlib/Probability/Notation.olean 999304 843824 .1555 Mathlib/Algebra/Order/Monoid/WithTop.olean 880096 842656 .0425 Mathlib/Algebra/Lie/UniversalEnveloping.olean 992088 838088 .1552 Mathlib/Order/Interval.olean 2225024 837976 .6233 Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.olean 854640 837968 .0195 Mathlib/Algebra/Group/WithOne/Defs.olean 892160 835192 .0638 Mathlib/Tactic/Linarith/Elimination.olean 841400 834232 .0085 Mathlib/Algebra/Hom/Aut.olean 1105192 828712 .2501 Mathlib/Data/Real/NNReal.olean 3209768 825456 .7428 Mathlib/RingTheory/IntegralClosure.olean 824288 824288 .0000 Mathlib/Tactic/CasesM.olean 1702456 822792 .5167 Mathlib/Algebra/GroupPower/Lemmas.olean 822592 822592 .0000 Mathlib/Algebra/Ring/ULift.olean 821832 821832 .0000 Mathlib/Tactic/HigherOrder.olean 835056 820416 .0175 Mathlib/Algebra/Category/Ring/Basic.olean 932056 820256 .1199 Mathlib/GroupTheory/NielsenSchreier.olean 1523800 820024 .4618 Mathlib/LinearAlgebra/Matrix/Basis.olean 1115544 818872 .2659 Mathlib/AlgebraicTopology/SplitSimplicialObject.olean 1511528 818800 .4582 Mathlib/Data/Set/Image.olean 1288976 818048 .3653 Mathlib/Topology/Algebra/Monoid.olean 1896688 816688 .5694 Mathlib/GroupTheory/OrderOfElement.olean 1212792 814280 .3285 Mathlib/FieldTheory/Galois.olean 1868712 812856 .5650 Mathlib/Computability/Primrec.olean 1888680 810864 .5706 Mathlib/AlgebraicTopology/SimplexCategory.olean 815848 810760 .0062 Mathlib/CategoryTheory/Category/ULift.olean 1063568 809344 .2390 Mathlib/MeasureTheory/Group/Arithmetic.olean 822568 809136 .0163 Mathlib/Data/Num/Basic.olean 868232 808744 .0685 Mathlib/Topology/Sets/Compacts.olean 994440 807992 .1874 Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.olean 1849312 805920 .5642 Mathlib/Topology/PathConnected.olean 815864 805624 .0125 Mathlib/Util/Superscript.olean 805288 805288 .0000 Mathlib/Data/ListM/DepthFirst.olean 804176 803544 .0007 Mathlib/Algebra/Order/Ring/InjSurj.olean 814176 800504 .0167 Mathlib/Algebra/Category/GroupCat/Limits.olean 827616 800072 .0332 Mathlib/Tactic/Backtracking.olean 1114472 799304 .2827 Mathlib/CategoryTheory/Sites/Subsheaf.olean 2228888 797792 .6420 Mathlib/Algebra/Order/Floor.olean 796168 796168 .0000 Mathlib/CategoryTheory/Limits/Preserves/Opposites.olean 797968 794864 .0038 Mathlib/AlgebraicTopology/SimplicialSet.olean 3557256 794808 .7765 Mathlib/Data/Complex/Exponential.olean 1731328 793792 .5415 Mathlib/Topology/Constructions.olean 939880 793008 .1562 Mathlib/Algebra/Ring/BooleanRing.olean 807392 792528 .0184 Mathlib/CategoryTheory/Triangulated/Rotate.olean 964232 792048 .1785 Mathlib/Algebra/Field/Basic.olean 1108640 790824 .2866 Mathlib/CategoryTheory/Abelian/Projective.olean 814728 790696 .0294 Mathlib/Data/Num/Bitwise.olean 938896 790144 .1584 Mathlib/GroupTheory/GroupAction/Quotient.olean 911736 788336 .1353 Mathlib/Logic/Encodable/Basic.olean 1040176 788024 .2424 Mathlib/NumberTheory/Padics/PadicIntegers.olean 1937960 784744 .5950 Mathlib/Data/Finset/Lattice.olean 797160 781320 .0198 Mathlib/CategoryTheory/Category/Pairwise.olean 829416 781112 .0582 Mathlib/Algebra/Category/GroupCat/Basic.olean 878240 780960 .1107 Mathlib/Logic/Equiv/List.olean 790360 780728 .0121 Mathlib/Tactic/Alias.olean 1602224 779752 .5133 Mathlib/Data/Matrix/Block.olean 779384 779384 .0000 Mathlib/Testing/SlimCheck/Sampleable.olean 902504 775880 .1403 Mathlib/Algebra/Module/Submodule/Lattice.olean 1112880 771808 .3064 Mathlib/CategoryTheory/Limits/Shapes/Diagonal.olean 1180832 770712 .3473 Mathlib/Order/BooleanAlgebra.olean 1233952 770472 .3756 Mathlib/CategoryTheory/Abelian/Exact.olean 1073872 770144 .2828 Mathlib/Data/Part.olean 897856 769488 .1429 Mathlib/Order/RelClasses.olean 842832 767760 .0890 Mathlib/Algebra/Order/Hom/Basic.olean 776736 767104 .0124 Mathlib/Geometry/Manifold/Instances/Real.olean 1145728 766224 .3312 Mathlib/LinearAlgebra/Projection.olean 1306288 765384 .4140 Mathlib/CategoryTheory/Limits/Shapes/CommSq.olean 800680 763888 .0459 Mathlib/Control/Monad/Cont.olean 768136 763416 .0061 Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.olean 1258656 763152 .3936 Mathlib/Data/PFun.olean 1413160 762496 .4604 Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.olean 865304 762400 .1189 Mathlib/GroupTheory/SpecificGroups/Dihedral.olean 792808 761336 .0396 Mathlib/CategoryTheory/Limits/Constructions/Equalizers.olean 760720 760720 .0000 Mathlib/Algebra/Category/Ring/FilteredColimits.olean 756864 756864 .0000 Mathlib/Tactic/Cases.olean 1559696 755096 .5158 Mathlib/Probability/Kernel/Composition.olean 754920 754368 .0007 Mathlib/Algebra/Field/ULift.olean 985824 753632 .2355 Mathlib/RingTheory/Ideal/LocalRing.olean 1851112 753392 .5930 Mathlib/Data/Polynomial/Eval.olean 2160544 751216 .6523 Mathlib/Data/Matrix/Notation.olean 1277280 750376 .4125 Mathlib/GroupTheory/NoncommPiCoprod.olean 1172984 749664 .3608 Mathlib/Analysis/Calculus/FDeriv/Mul.olean 1557464 748960 .5191 Mathlib/Data/PFunctor/Univariate/M.olean 2716520 748504 .7244 Mathlib/LinearAlgebra/LinearIndependent.olean 1018920 746928 .2669 Mathlib/ModelTheory/ElementaryMaps.olean 1291848 744656 .4235 Mathlib/Topology/Algebra/Module/FiniteDimension.olean 889584 743840 .1638 Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.olean 1392568 741232 .4677 Mathlib/Data/List/Sigma.olean 796520 741032 .0696 Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.olean 1086552 740632 .3183 Mathlib/Topology/Sheaves/LocalPredicate.olean 747928 739984 .0106 Mathlib/Algebra/DirectSum/Algebra.olean 864416 738824 .1452 Mathlib/Algebra/Category/ModuleCat/FilteredColimits.olean 930752 738600 .2064 Mathlib/Data/Sym/Basic.olean 799896 737024 .0786 Mathlib/Tactic/NormNum/Prime.olean 788856 735856 .0671 Mathlib/CategoryTheory/Category/Bipointed.olean 798504 735640 .0787 Mathlib/CategoryTheory/Functor/Category.olean 1777552 734456 .5868 Mathlib/Topology/Algebra/InfiniteSum/Basic.olean 773440 733520 .0516 Mathlib/Logic/Embedding/Basic.olean 771920 731328 .0525 Mathlib/LinearAlgebra/UnitaryGroup.olean 1154264 730344 .3672 Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.olean 1019472 729560 .2843 Mathlib/Analysis/Normed/Group/Quotient.olean 749256 728544 .0276 Mathlib/Algebra/Category/MonCat/Basic.olean 1729488 728416 .5788 Mathlib/Order/Filter/AtTopBot.olean 738608 728144 .0141 Mathlib/Tactic/GeneralizeProofs.olean 727648 727648 .0000 Mathlib/Tactic/FieldSimp.olean 801784 726768 .0935 Mathlib/Algebra/Tropical/Basic.olean 784592 725536 .0752 Mathlib/Algebra/Category/ModuleCat/Kernels.olean 1911736 725352 .6205 Mathlib/Algebra/BigOperators/Finprod.olean 1070840 722960 .3248 Mathlib/MeasureTheory/Group/Measure.olean 792856 720448 .0913 Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.olean 725392 718536 .0094 Mathlib/CategoryTheory/Monoidal/FunctorCategory.olean 731552 718344 .0180 Mathlib/CategoryTheory/Bicategory/FunctorBicategory.olean 904224 718136 .2057 Mathlib/Combinatorics/SimpleGraph/Prod.olean 1143368 717656 .3723 Mathlib/RingTheory/FreeCommRing.olean 830360 716072 .1376 Mathlib/CategoryTheory/Subobject/Comma.olean 1053392 715968 .3203 Mathlib/NumberTheory/Padics/Hensel.olean 718272 714816 .0048 Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.olean 1416576 713680 .4961 Mathlib/Order/Filter/Bases.olean 912288 713544 .2178 Mathlib/CategoryTheory/Iso.olean 713144 713144 .0000 Mathlib/Tactic/Conv.olean 843480 711920 .1559 Mathlib/Algebra/DirectSum/Decomposition.olean 803560 709816 .1166 Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.olean 829056 709792 .1438 Mathlib/Algebra/Star/Basic.olean 1177544 708656 .3981 Mathlib/Data/Set/Pointwise/SMul.olean 796952 706696 .1132 Mathlib/CategoryTheory/Closed/Cartesian.olean 978240 704672 .2796 Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.olean 788360 704552 .1063 Mathlib/CategoryTheory/Idempotents/FunctorCategories.olean 708096 702792 .0074 Mathlib/Algebra/Ring/Pi.olean 1254848 701568 .4409 Mathlib/Topology/MetricSpace/PiNat.olean 1032768 701232 .3210 Mathlib/Analysis/SpecialFunctions/Bernstein.olean 1339208 701200 .4764 Mathlib/NumberTheory/Padics/PadicNumbers.olean 1217712 698720 .4262 Mathlib/Data/Polynomial/AlgebraMap.olean 707368 698672 .0122 Mathlib/CategoryTheory/Adjunction/Comma.olean 972304 698608 .2814 Mathlib/CategoryTheory/Preadditive/HomOrthogonal.olean 731752 698528 .0454 Mathlib/CategoryTheory/Sites/Whiskering.olean 893464 697960 .2188 Mathlib/AlgebraicGeometry/LocallyRingedSpace.olean 1401688 697448 .5024 Mathlib/Topology/ContinuousFunction/Ideals.olean 697648 696864 .0011 Mathlib/Tactic/Nontriviality/Core.olean 1454752 694568 .5225 Mathlib/Data/Set/Function.olean 727640 693608 .0467 Mathlib/Topology/UniformSpace/Equiv.olean 722752 693472 .0405 Mathlib/Mathport/Rename.olean 1297832 692040 .4667 Mathlib/GroupTheory/Complement.olean 853824 689256 .1927 Mathlib/Data/LazyList/Basic.olean 717888 689024 .0402 Mathlib/Tactic/Cache.olean 1020320 687384 .3263 Mathlib/RingTheory/Localization/Ideal.olean 684504 684504 .0000 Mathlib/Tactic/ProjectionNotation.olean 787720 682968 .1329 Mathlib/Order/Ideal.olean 709344 681072 .0398 Mathlib/Algebra/Category/GroupCat/Biproducts.olean 1800232 680552 .6219 Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.olean 938800 679960 .2757 Mathlib/GroupTheory/GroupAction/Basic.olean 763288 677752 .1120 Mathlib/Analysis/InnerProductSpace/Dual.olean 2286688 676512 .7041 Mathlib/LinearAlgebra/Dimension.olean 888104 676344 .2384 Mathlib/Logic/Equiv/Fin.olean 1635264 675480 .5869 Mathlib/RingTheory/Algebraic.olean 1026232 675120 .3421 Mathlib/NumberTheory/LucasLehmer.olean 718464 674704 .0609 Mathlib/Data/Set/Intervals/Instances.olean 1417472 674560 .5241 Mathlib/Analysis/SpecialFunctions/Pow/Real.olean 787368 674432 .1434 Mathlib/Data/Setoid/Basic.olean 717096 674256 .0597 Mathlib/CategoryTheory/Adjunction/FullyFaithful.olean 2219288 674192 .6962 Mathlib/Data/Polynomial/RingDivision.olean 2112240 674032 .6808 Mathlib/MeasureTheory/Integral/SetIntegral.olean 756160 673872 .1088 Mathlib/Topology/ContinuousFunction/Basic.olean 1014720 673560 .3362 Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.olean 1699416 673448 .6037 Mathlib/NumberTheory/PythagoreanTriples.olean 1107152 673304 .3918 Mathlib/Topology/UniformSpace/CompactConvergence.olean 2081872 671848 .6772 Mathlib/LinearAlgebra/Matrix/Determinant.olean 682504 671192 .0165 Mathlib/Algebra/Order/Pi.olean 676432 671160 .0077 Mathlib/Tactic/SplitIfs.olean 1393616 669288 .5197 Mathlib/Order/LiminfLimsup.olean 1770688 665576 .6241 Mathlib/MeasureTheory/Integral/DivergenceTheorem.olean 726208 664064 .0855 Mathlib/Algebra/Star/Module.olean 1061512 661512 .3768 Mathlib/CategoryTheory/Sites/CompatiblePlus.olean 701456 659624 .0596 Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.olean 685040 658688 .0384 Mathlib/Data/Polynomial/Identities.olean 683880 658096 .0377 Mathlib/Algebra/Field/Defs.olean 819552 658096 .1970 Mathlib/MeasureTheory/Integral/Average.olean 765264 657992 .1401 Mathlib/Algebra/Order/AbsoluteValue.olean 790616 657384 .1685 Mathlib/GroupTheory/Subsemigroup/Basic.olean 1549880 657232 .5759 Mathlib/LinearAlgebra/Orientation.olean 1384696 656936 .5255 Mathlib/LinearAlgebra/Lagrange.olean 800176 656568 .1794 Mathlib/CategoryTheory/Limits/Types.olean 749032 653408 .1276 Mathlib/Analysis/NormedSpace/Star/Basic.olean 1339016 651456 .5134 Mathlib/GroupTheory/SpecificGroups/Cyclic.olean 653904 650696 .0049 Mathlib/CategoryTheory/Linear/Basic.olean 696752 648744 .0689 Mathlib/Topology/Algebra/Module/WeakDual.olean 1488112 648248 .5643 Mathlib/Data/Fin/Tuple/Basic.olean 820048 648024 .2097 Mathlib/Topology/MetricSpace/Isometry.olean 849680 647696 .2377 Mathlib/CategoryTheory/Abelian/NonPreadditive.olean 816528 647376 .2071 Mathlib/Data/Analysis/Topology.olean 1079000 647184 .4002 Mathlib/Computability/RegularExpressions.olean 971720 646840 .3343 Mathlib/GroupTheory/Submonoid/Pointwise.olean 992088 646232 .3486 Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.olean 747744 645296 .1370 Mathlib/CategoryTheory/Category/Basic.olean 1196152 644696 .4610 Mathlib/Topology/UniformSpace/UniformEmbedding.olean 1071416 644336 .3986 Mathlib/Topology/Order.olean 773824 643776 .1680 Mathlib/Topology/Algebra/OpenSubgroup.olean 717624 641728 .1057 Mathlib/Algebra/Homology/Homology.olean 1647384 640536 .6111 Mathlib/Data/Polynomial/Div.olean 1001808 640312 .3608 Mathlib/Logic/Function/Basic.olean 825064 638160 .2265 Mathlib/Topology/Sets/Opens.olean 731352 637816 .1278 Mathlib/CategoryTheory/Arrow.olean 909336 635672 .3009 Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.olean 989888 634576 .3589 Mathlib/Data/MvPolynomial/Monad.olean 634144 634144 .0000 Mathlib/Tactic/ToExpr.olean 654480 634000 .0312 Mathlib/Tactic/Group.olean 633608 633608 .0000 Mathlib/Tactic/Relation/Rfl.olean 634232 632312 .0030 Mathlib/CategoryTheory/Products/Associator.olean 921512 631672 .3145 Mathlib/CategoryTheory/Subobject/Limits.olean 1514272 630440 .5836 Mathlib/Data/List/BigOperators/Basic.olean 687848 628696 .0859 Mathlib/Init/Logic.olean 900552 628256 .3023 Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.olean 1022880 628192 .3858 Mathlib/Data/Sign.olean 1170632 627464 .4639 Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.olean 1900376 626328 .6704 Mathlib/Analysis/Convex/Segment.olean 971624 624376 .3573 Mathlib/Data/Nat/Basic.olean 843448 623000 .2613 Mathlib/Analysis/Complex/Basic.olean 1031280 620832 .3979 Mathlib/GroupTheory/Perm/Basic.olean 748408 619792 .1718 Mathlib/CategoryTheory/Limits/Shapes/Products.olean 1093208 619712 .4331 Mathlib/FieldTheory/Fixed.olean 750472 619584 .1744 Mathlib/CategoryTheory/Localization/Predicate.olean 686456 618080 .0996 Mathlib/Topology/Order/Hom/Esakia.olean 743320 616432 .1707 Mathlib/Data/Vector3.olean 687880 615296 .1055 Mathlib/CategoryTheory/Preadditive/ProjectiveResolution.olean 634296 614088 .0318 Mathlib/Data/Prod/Lex.olean 885296 613648 .3068 Mathlib/Algebra/Order/CompleteField.olean 831584 612584 .2633 Mathlib/Algebra/Algebra/Tower.olean 1513264 612312 .5953 Mathlib/Data/Polynomial/Degree/Definitions.olean 813672 611592 .2483 Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.olean 1369680 611520 .5535 Mathlib/MeasureTheory/Integral/FundThmCalculus.olean 699056 611472 .1252 Mathlib/Topology/Category/Profinite/Basic.olean 697608 608232 .1281 Mathlib/Analysis/Normed/Group/AddTorsor.olean 723152 607560 .1598 Mathlib/Topology/UniformSpace/AbstractCompletion.olean 636800 605632 .0489 Mathlib/GroupTheory/GroupAction/ConjAct.olean 776560 604776 .2212 Mathlib/Topology/Category/Compactum.olean 708112 603752 .1473 Mathlib/Data/Finsupp/ToDfinsupp.olean 1004576 602400 .4003 Mathlib/Algebra/Order/Monoid/Lemmas.olean 736512 601904 .1827 Mathlib/CategoryTheory/Sites/Adjunction.olean 603288 601576 .0028 Mathlib/CategoryTheory/Bicategory/SingleObj.olean 1043512 601104 .4239 Mathlib/LinearAlgebra/AffineSpace/Basis.olean 779560 600424 .2297 Mathlib/Analysis/NormedSpace/Star/Spectrum.olean 661952 599272 .0946 Mathlib/CategoryTheory/LiftingProperties/Adjunction.olean 759680 597512 .2134 Mathlib/Order/BoundedOrder.olean 947992 595448 .3718 Mathlib/Data/Holor.olean 597800 594016 .0063 Mathlib/Topology/Category/TopCat/OpenNhds.olean 1058928 593512 .4395 Mathlib/Data/List/Sort.olean 1683680 591784 .6485 Mathlib/MeasureTheory/Decomposition/Lebesgue.olean 864088 591720 .3152 Mathlib/Data/List/Func.olean 646752 591296 .0857 Mathlib/LinearAlgebra/QuadraticForm/Isometry.olean 1437440 591200 .5887 Mathlib/Data/Set/Intervals/Basic.olean 599384 591152 .0137 Mathlib/Algebra/GroupWithZero/InjSurj.olean 959288 590456 .3844 Mathlib/Data/Real/EReal.olean 592488 590184 .0038 Mathlib/Algebra/Homology/Functor.olean 645464 590072 .0858 Mathlib/Analysis/Normed/Ring/Seminorm.olean 970584 589032 .3931 Mathlib/Analysis/InnerProductSpace/Orthogonal.olean 1057480 588808 .4431 Mathlib/Topology/Algebra/ValuedField.olean 1114968 588552 .4721 Mathlib/MeasureTheory/Constructions/Pi.olean 1407248 588280 .5819 Mathlib/Analysis/Calculus/Inverse.olean 1225744 588096 .5202 Mathlib/RingTheory/Polynomial/Chebyshev.olean 1298048 587720 .5472 Mathlib/LinearAlgebra/Ray.olean 710248 587248 .1731 Mathlib/Logic/Equiv/Option.olean 585208 585208 .0000 Mathlib/Tactic/Convert.olean 587968 585120 .0048 Mathlib/Algebra/DualQuaternion.olean 823048 583832 .2906 Mathlib/NumberTheory/LegendreSymbol/MulCharacter.olean 632000 583656 .0764 Mathlib/Order/Category/SemilatCat.olean 792496 583328 .2639 Mathlib/Data/Real/Sqrt.olean 963976 581480 .3967 Mathlib/MeasureTheory/Integral/TorusIntegral.olean 607048 579896 .0447 Mathlib/Tactic/WLOG.olean 585912 579768 .0104 Mathlib/Algebra/Homology/LocalCohomology.olean 587688 578520 .0156 Mathlib/CategoryTheory/Limits/Over.olean 826472 578040 .3005 Mathlib/Topology/UniformSpace/Separation.olean 593344 577416 .0268 Mathlib/Analysis/VonNeumannAlgebra/Basic.olean 1062232 574992 .4586 Mathlib/Analysis/BoxIntegral/Partition/Basic.olean 1755224 573296 .6733 Mathlib/Analysis/BoxIntegral/Basic.olean 1976240 572856 .7101 Mathlib/MeasureTheory/Function/LpSeminorm.olean 1549232 572480 .6304 Mathlib/Topology/Instances/ENNReal.olean 629248 570320 .0936 Mathlib/Combinatorics/Quiver/Basic.olean 651656 569648 .1258 Mathlib/Order/Category/NonemptyFinLinOrdCat.olean 1144352 569112 .5026 Mathlib/GroupTheory/Submonoid/Membership.olean 1402096 567168 .5954 Mathlib/Analysis/NormedSpace/Banach.olean 1365280 566304 .5852 Mathlib/Analysis/Calculus/FDeriv/Basic.olean 902328 564632 .3742 Mathlib/Data/Fintype/Card.olean 563896 563896 .0000 Mathlib/Tactic/Find.olean 566536 563224 .0058 Mathlib/CategoryTheory/Monad/Kleisli.olean 578480 562784 .0271 Mathlib/Tactic/Simps/NotationClass.olean 562544 562544 .0000 Mathlib/Tactic/SimpIntro.olean 659408 560064 .1506 Mathlib/Algebra/Order/WithZero.olean 1334824 557224 .5825 Mathlib/Algebra/Order/ToIntervalMod.olean 557920 556848 .0019 Mathlib/Control/Monad/Writer.olean 565520 556688 .0156 Mathlib/CategoryTheory/Endomorphism.olean 556488 556488 .0000 Mathlib/Tactic/Set.olean 1062368 555080 .4775 Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.olean 582760 554544 .0484 Mathlib/Order/Circular.olean 649576 554120 .1469 Mathlib/Init/Algebra/Order.olean 699328 553024 .2092 Mathlib/Algebra/LinearRecurrence.olean 1231104 552672 .5510 Mathlib/RingTheory/ChainOfDivisors.olean 667192 551248 .1737 Mathlib/CategoryTheory/PathCategory.olean 553056 551064 .0036 Mathlib/Logic/Equiv/Embedding.olean 899864 549896 .3889 Mathlib/Data/Fin/VecNotation.olean 1701952 549296 .6772 Mathlib/RingTheory/Finiteness.olean 796920 548808 .3113 Mathlib/Algebra/Hom/Units.olean 760744 548712 .2787 Mathlib/LinearAlgebra/SymplecticGroup.olean 1586344 547320 .6549 Mathlib/Topology/Connected.olean 1331784 545320 .5905 Mathlib/NumberTheory/Padics/RingHoms.olean 799600 543800 .3199 Mathlib/Probability/Kernel/Basic.olean 649080 540928 .1666 Mathlib/Data/List/Lex.olean 1378856 540600 .6079 Mathlib/Data/List/Zip.olean 1548600 540064 .6512 Mathlib/RingTheory/ClassGroup.olean 619120 539152 .1291 Mathlib/Algebra/FreeMonoid/Basic.olean 657024 536984 .1827 Mathlib/Data/Dfinsupp/Order.olean 1237040 536592 .5662 Mathlib/Data/Polynomial/Module.olean 647368 536360 .1714 Mathlib/InformationTheory/Hamming.olean 542144 536280 .0108 Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.olean 688904 535504 .2226 Mathlib/Logic/Denumerable.olean 544160 535152 .0165 Mathlib/CategoryTheory/Monoidal/Opposite.olean 1013816 534936 .4723 Mathlib/Algebra/BigOperators/Finsupp.olean 561144 534632 .0472 Mathlib/Data/Finset/Functor.olean 1189616 534632 .5505 Mathlib/Data/PFunctor/Multivariate/M.olean 534112 534112 .0000 Mathlib/Tactic/FinCases.olean 614504 534096 .1308 Mathlib/AlgebraicTopology/MooreComplex.olean 583528 532528 .0873 Mathlib/CategoryTheory/Sites/Pretopology.olean 639560 531808 .1684 Mathlib/Algebra/Invertible.olean 582144 530144 .0893 Mathlib/Topology/Algebra/Ring/Basic.olean 530000 530000 .0000 Mathlib/Data/Bitvec/Defs.olean 529528 529528 .0000 Mathlib/Tactic/Have.olean 789440 529512 .3292 Mathlib/FieldTheory/SplittingField/Construction.olean 826808 527952 .3614 Mathlib/Algebra/Homology/ShortComplex/RightHomology.olean 770136 524736 .3186 Mathlib/CategoryTheory/Triangulated/Basic.olean 568152 523960 .0777 Mathlib/Combinatorics/SimpleGraph/Finsubgraph.olean 537232 522320 .0277 Mathlib/Order/Category/FinBoolAlgCat.olean 570576 522040 .0850 Mathlib/Data/Bitvec/Core.olean 523624 521688 .0036 Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.olean 689808 521280 .2443 Mathlib/Computability/Reduce.olean 810096 520912 .3569 Mathlib/GroupTheory/Torsion.olean 969680 519048 .4647 Mathlib/Data/QPF/Univariate/Basic.olean 518472 518472 .0000 Mathlib/Algebra/Order/Field/InjSurj.olean 603064 517784 .1414 Mathlib/Analysis/NormedSpace/ContinuousLinearMap.olean 1082952 517112 .5224 Mathlib/Topology/Category/TopCat/Limits/Pullbacks.olean 517056 517056 .0000 Mathlib/Tactic/SlimCheck.olean 516496 516496 .0000 Mathlib/Tactic/Widget/CommDiag.olean 561712 513944 .0850 Mathlib/Topology/Algebra/GroupCompletion.olean 866120 513296 .4073 Mathlib/CategoryTheory/CofilteredSystem.olean 2065224 512320 .7519 Mathlib/LinearAlgebra/AffineSpace/Independent.olean 1043520 512240 .5091 Mathlib/CategoryTheory/Sites/CoverLifting.olean 588616 511680 .1307 Mathlib/Data/FP/Basic.olean 1563600 510760 .6733 Mathlib/Analysis/LocallyConvex/WithSeminorms.olean 510728 510728 .0000 Mathlib/Data/Stream/Defs.olean 810640 510112 .3707 Mathlib/RingTheory/Henselian.olean 527032 508320 .0355 Mathlib/Analysis/Normed/Field/UnitBall.olean 1267080 507672 .5993 Mathlib/MeasureTheory/Integral/CircleIntegral.olean 678152 507328 .2518 Mathlib/Topology/Algebra/ConstMulAction.olean 860040 506664 .4108 Mathlib/RingTheory/Adjoin/PowerBasis.olean 853120 506392 .4064 Mathlib/Logic/Basic.olean 1296280 506168 .6095 Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.olean 802160 502968 .3729 Mathlib/Computability/TMComputable.olean 505792 502760 .0059 Mathlib/LinearAlgebra/Multilinear/TensorProduct.olean 883376 502544 .4311 Mathlib/Algebra/QuaternionBasis.olean 1914744 502376 .7376 Mathlib/MeasureTheory/Covering/Besicovitch.olean 1167576 502104 .5699 Mathlib/Data/List/Rotate.olean 525520 501600 .0455 Mathlib/Order/Antisymmetrization.olean 569384 501600 .1190 Mathlib/Topology/Sets/Closeds.olean 1464896 501440 .6576 Mathlib/Analysis/Convex/Function.olean 604488 501200 .1708 Mathlib/CategoryTheory/Quotient.olean 1014080 499952 .5069 Mathlib/Data/Finset/Image.olean 1832640 499320 .7275 Mathlib/Algebra/Lie/Nilpotent.olean 605944 499168 .1762 Mathlib/Analysis/NormedSpace/ENorm.olean 510840 498736 .0236 Mathlib/GroupTheory/Divisible.olean 1219568 498736 .5910 Mathlib/GroupTheory/Perm/Cycle/Type.olean 511272 498712 .0245 Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.olean 677464 498264 .2645 Mathlib/Probability/Process/Filtration.olean 730024 496952 .3192 Mathlib/Data/List/AList.olean 1070200 495288 .5372 Mathlib/MeasureTheory/Function/L2Space.olean 583288 494792 .1517 Mathlib/CategoryTheory/Closed/Monoidal.olean 861776 494096 .4266 Mathlib/LinearAlgebra/CrossProduct.olean 493984 493984 .0000 Mathlib/Util/WhatsNew.olean 651224 492704 .2434 Mathlib/Order/Filter/Ultrafilter.olean 602656 492616 .1825 Mathlib/Topology/Category/CompHaus/Basic.olean 495040 492320 .0054 Mathlib/CategoryTheory/ConnectedComponents.olean 936312 492032 .4745 Mathlib/Order/Bounds/Basic.olean 647576 491696 .2407 Mathlib/Topology/MetricSpace/IsometricSMul.olean 492848 490968 .0038 Mathlib/CategoryTheory/Subobject/Types.olean 1200664 489504 .5923 Mathlib/Topology/ContinuousOn.olean 715064 489072 .3160 Mathlib/Algebra/Lie/Solvable.olean 754760 488824 .3523 Mathlib/Combinatorics/Colex.olean 726304 488344 .3276 Mathlib/AlgebraicGeometry/Scheme.olean 1114168 487920 .5620 Mathlib/Data/Nat/Factorization/Basic.olean 514720 487496 .0528 Mathlib/Topology/Category/CompHaus/ExplicitLimits.olean 487456 487280 .0003 Mathlib/Tactic/ModCases.olean 502016 487080 .0297 Mathlib/Topology/Sheaves/Operations.olean 535624 485464 .0936 Mathlib/Algebra/Algebra/Bilinear.olean 1731456 484656 .7200 Mathlib/MeasureTheory/Measure/Haar/Basic.olean 630312 484256 .2317 Mathlib/CategoryTheory/Abelian/Opposite.olean 489584 484192 .0110 Mathlib/Algebra/Algebra/Pi.olean 1179832 480984 .5923 Mathlib/CategoryTheory/Abelian/Pseudoelements.olean 642752 479800 .2535 Mathlib/AlgebraicTopology/DoldKan/Compatibility.olean 512576 478912 .0656 Mathlib/Data/Tree.olean 1189384 476976 .5989 Mathlib/RingTheory/Ideal/Basic.olean 1813952 476896 .7370 Mathlib/MeasureTheory/Measure/Hausdorff.olean 1515312 476560 .6855 Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.olean 1335872 476536 .6432 Mathlib/RingTheory/WittVector/StructurePolynomial.olean 476336 476336 .0000 Mathlib/Tactic/Recover.olean 806320 475952 .4097 Mathlib/RingTheory/WittVector/Defs.olean 937080 474440 .4937 Mathlib/Topology/CompactOpen.olean 474408 474408 .0000 Mathlib/CategoryTheory/Monoidal/Rigid/FunctorCategory.olean 475040 473568 .0030 Mathlib/Order/Category/PartOrdCat.olean 514376 473368 .0797 Mathlib/CategoryTheory/Types.olean 924352 472552 .4887 Mathlib/Data/Stream/Init.olean 1026968 472528 .5398 Mathlib/Analysis/NormedSpace/Exponential.olean 1258064 471848 .6249 Mathlib/Order/JordanHolder.olean 948936 471624 .5029 Mathlib/CategoryTheory/Abelian/RightDerived.olean 635592 471024 .2589 Mathlib/Data/Fintype/Perm.olean 1629608 471016 .7109 Mathlib/LinearAlgebra/Matrix/Adjugate.olean 569088 470680 .1729 Mathlib/LinearAlgebra/ProjectiveSpace/Basic.olean 584408 470424 .1950 Mathlib/GroupTheory/GroupAction/Group.olean 638672 469472 .2649 Mathlib/Algebra/Order/Monoid/Canonical/Defs.olean 478776 469440 .0194 Mathlib/Analysis/NormedSpace/BallAction.olean 785608 469304 .4026 Mathlib/Data/Sum/Basic.olean 558608 469288 .1598 Mathlib/CategoryTheory/NatIso.olean 469816 468488 .0028 Mathlib/Topology/Sheaves/PresheafOfFunctions.olean 503024 468328 .0689 Mathlib/Algebra/SMulWithZero.olean 975800 466640 .5217 Mathlib/Analysis/NormedSpace/CompactOperator.olean 468976 466128 .0060 Mathlib/Algebra/Module/ULift.olean 1515776 465360 .6929 Mathlib/CategoryTheory/Filtered.olean 1008616 465312 .5386 Mathlib/GroupTheory/Nilpotent.olean 464640 464640 .0000 Mathlib/Tactic/LabelAttr.olean 882192 464136 .4738 Mathlib/Analysis/ODE/PicardLindelof.olean 515744 463296 .1016 Mathlib/CategoryTheory/Limits/Lattice.olean 1466792 462872 .6844 Mathlib/Data/Polynomial/FieldDivision.olean 466256 461544 .0101 Mathlib/CategoryTheory/Monoidal/Limits.olean 789488 461072 .4159 Mathlib/FieldTheory/IsAlgClosed/Spectrum.olean 481848 460736 .0438 Mathlib/Algebra/DualNumber.olean 828848 459704 .4453 Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.olean 517480 459616 .1118 Mathlib/GroupTheory/GroupAction/Pi.olean 622040 459592 .2611 Mathlib/Topology/UniformSpace/Compact.olean 626368 458848 .2674 Mathlib/Algebra/Order/UpperLower.olean 473472 458376 .0318 Mathlib/Order/Category/FinPartOrd.olean 759896 456656 .3990 Mathlib/Data/List/Infix.olean 775448 456536 .4112 Mathlib/Analysis/Fourier/FourierTransform.olean 497576 455024 .0855 Mathlib/Topology/Algebra/Algebra.olean 582712 454960 .2192 Mathlib/Data/Pi/Lex.olean 1263416 454592 .6401 Mathlib/MeasureTheory/Group/FundamentalDomain.olean 499504 453736 .0916 Mathlib/CategoryTheory/Subterminal.olean 468736 453192 .0331 Mathlib/Data/ZMod/Defs.olean 864816 452440 .4768 Mathlib/Data/Real/Pi/Bounds.olean 691832 450192 .3492 Mathlib/Topology/Inseparable.olean 1187424 450136 .6209 Mathlib/Geometry/Euclidean/Basic.olean 944904 449752 .5240 Mathlib/GroupTheory/Subgroup/Pointwise.olean 590224 449360 .2386 Mathlib/Data/Dfinsupp/Interval.olean 510896 449184 .1207 Mathlib/GroupTheory/GroupAction/SubMulAction.olean 1307576 448744 .6568 Mathlib/RingTheory/AlgebraicIndependent.olean 450120 448264 .0041 Mathlib/Algebra/Order/Positive/Ring.olean 468240 447680 .0439 Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.olean 1093872 447136 .5912 Mathlib/Data/Polynomial/Splits.olean 1210880 446632 .6311 Mathlib/LinearAlgebra/Eigenspace/Basic.olean 447568 446344 .0027 Mathlib/Algebra/Field/Opposite.olean 713368 446152 .3745 Mathlib/Analysis/BoxIntegral/Partition/Filter.olean 601400 445512 .2592 Mathlib/Order/Chain.olean 486200 445104 .0845 Mathlib/CategoryTheory/ConcreteCategory/BundledHom.olean 478664 444616 .0711 Mathlib/Algebra/Group/WithOne/Basic.olean 444064 444064 .0000 Mathlib/Tactic/TryThis.olean 459424 443760 .0340 Mathlib/Algebra/Algebra/Prod.olean 860368 441216 .4871 Mathlib/RingTheory/Polynomial/Quotient.olean 569752 440888 .2261 Mathlib/Data/Setoid/Partition.olean 443000 440824 .0049 Mathlib/RingTheory/Valuation/ExtendToLocalization.olean 2269032 439656 .8062 Mathlib/Geometry/Euclidean/Circumcenter.olean 827256 438536 .4698 Mathlib/Analysis/Calculus/BumpFunctionInner.olean 1226560 438416 .6425 Mathlib/SetTheory/Cardinal/Ordinal.olean 1245152 438104 .6481 Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.olean 469648 437088 .0693 Mathlib/Init/Algebra/Classes.olean 576816 436728 .2428 Mathlib/GroupTheory/Submonoid/Inverses.olean 588896 435680 .2601 Mathlib/Algebra/AddTorsor.olean 532136 435328 .1819 Mathlib/Order/ModularLattice.olean 682072 435072 .3621 Mathlib/Data/Nat/PartENat.olean 563408 434080 .2295 Mathlib/GroupTheory/Abelianization.olean 434392 433928 .0010 Mathlib/Init/Set.olean 893496 433712 .5145 Mathlib/AlgebraicTopology/DoldKan/NCompGamma.olean 588240 433000 .2639 Mathlib/MeasureTheory/MeasurableSpaceDef.olean 434480 432128 .0054 Mathlib/Algebra/PUnitInstances.olean 461544 431368 .0653 Mathlib/Algebra/Opposites.olean 430656 430656 .0000 Mathlib/Tactic/CategoryTheory/Slice.olean 451192 429920 .0471 Mathlib/Algebra/Homology/HomotopyCategory.olean 500616 429752 .1415 Mathlib/Control/Basic.olean 1069328 429576 .5982 Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.olean 811608 429152 .4712 Mathlib/Data/List/Chain.olean 791672 428432 .4588 Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.olean 650368 428256 .3415 Mathlib/Logic/Relation.olean 929352 428184 .5392 Mathlib/Data/Polynomial/Laurent.olean 1535832 427736 .7214 Mathlib/LinearAlgebra/Matrix/Transvection.olean 465224 426168 .0839 Mathlib/Algebra/GroupWithZero/Defs.olean 1129056 425000 .6235 Mathlib/Algebra/Group/Basic.olean 1218104 424952 .6511 Mathlib/Analysis/Calculus/FDeriv/Equiv.olean 1652504 424704 .7429 Mathlib/Algebra/CubicDiscriminant.olean 438616 424120 .0330 Mathlib/Data/BinaryHeap.olean 423896 423896 .0000 Mathlib/Tactic/NthRewrite.olean 432296 423440 .0204 Mathlib/CategoryTheory/Limits/Constructions/Filtered.olean 918032 423440 .5387 Mathlib/Data/Seq/Parallel.olean 423232 423232 .0000 Mathlib/Algebra/Order/Field/Canonical/Defs.olean 421680 421680 .0000 Mathlib/CategoryTheory/Monoidal/Internal/Types.olean 1371560 419328 .6942 Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.olean 1359208 419264 .6915 Mathlib/Analysis/Calculus/MeanValue.olean 529896 418520 .2101 Mathlib/Algebra/MonoidAlgebra/ToDirectSum.olean 484872 418000 .1379 Mathlib/CategoryTheory/Adjunction/Reflective.olean 1015136 417928 .5883 Mathlib/Order/Filter/Prod.olean 417888 417888 .0000 Mathlib/Tactic/Slice.olean 1314736 417872 .6821 Mathlib/Probability/Process/Stopping.olean 738216 417808 .4340 Mathlib/Topology/PartitionOfUnity.olean 417576 417576 .0000 Mathlib/Tactic/SudoSetOption.olean 418848 417568 .0030 Mathlib/Analysis/Normed/Order/Basic.olean 427480 417136 .0241 Mathlib/Tactic/PrintPrefix.olean 434608 417088 .0403 Mathlib/CategoryTheory/Closed/FunctorCategory.olean 1564424 417024 .7334 Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.olean 1258152 416872 .6686 Mathlib/Deprecated/Subgroup.olean 1041144 416240 .6002 Mathlib/MeasureTheory/PiSystem.olean 529856 416136 .2146 Mathlib/Init/Data/Nat/Lemmas.olean 1239720 415920 .6645 Mathlib/Computability/Partrec.olean 659616 415528 .3700 Mathlib/Algebra/Order/Ring/Lemmas.olean 472984 415240 .1220 Mathlib/Algebra/Module/Submodule/Pointwise.olean 634360 414912 .3459 Mathlib/Combinatorics/Quiver/Path.olean 731024 414408 .4331 Mathlib/RingTheory/IntegralDomain.olean 692392 413944 .4021 Mathlib/Topology/Algebra/StarSubalgebra.olean 767040 413784 .4605 Mathlib/Order/SymmDiff.olean 413576 413576 .0000 Mathlib/Tactic/Coe.olean 838160 413472 .5066 Mathlib/Combinatorics/Configuration.olean 723872 413160 .4292 Mathlib/Analysis/BoxIntegral/Box/Basic.olean 575504 412848 .2826 Mathlib/RingTheory/Valuation/Integers.olean 1011896 412720 .5921 Mathlib/Data/List/Sublists.olean 512768 412048 .1964 Mathlib/Analysis/NormedSpace/WeakDual.olean 1021336 411600 .5969 Mathlib/Topology/UniformSpace/Cauchy.olean 701992 411296 .4141 Mathlib/Data/MvPolynomial/Derivation.olean 466352 411088 .1185 Mathlib/Analysis/NormedSpace/LpEquiv.olean 700472 410992 .4132 Mathlib/Topology/UniformSpace/Completion.olean 493152 410560 .1674 Mathlib/Topology/Homotopy/Equiv.olean 433848 410136 .0546 Mathlib/Topology/Category/TopCommRingCat.olean 521792 408944 .2162 Mathlib/Data/Prod/Basic.olean 407304 407304 .0000 Mathlib/Tactic/SimpRw.olean 1214456 406992 .6648 Mathlib/Topology/MetricSpace/HausdorffDistance.olean 498968 406768 .1847 Mathlib/Order/Concept.olean 409088 406552 .0061 Mathlib/Topology/MetricSpace/EMetricParacompact.olean 434360 406104 .0650 Mathlib/Topology/Instances/TrivSqZeroExt.olean 405352 405352 .0000 Mathlib/Lean/Meta/DiscrTree.olean 428512 404552 .0559 Mathlib/Order/Grade.olean 1676080 404480 .7586 Mathlib/Analysis/Convex/Side.olean 407104 403544 .0087 Mathlib/CategoryTheory/Monad/Coequalizer.olean 434664 402800 .0733 Mathlib/Order/Hom/Order.olean 435664 402536 .0760 Mathlib/CategoryTheory/Functor/Basic.olean 622472 402000 .3541 Mathlib/Data/Finset/Sups.olean 924312 401024 .5661 Mathlib/CategoryTheory/Monoidal/Preadditive.olean 578800 400728 .3076 Mathlib/Topology/Compactification/OnePoint.olean 431688 400320 .0726 Mathlib/Tactic/NormNum/NatFib.olean 797696 400152 .4983 Mathlib/Analysis/InnerProductSpace/Calculus.olean 402264 400024 .0055 Mathlib/CategoryTheory/Category/Cat.olean 495392 399200 .1941 Mathlib/Analysis/Quaternion.olean 1423952 397184 .7210 Mathlib/Data/MvPolynomial/Variables.olean 1243928 397016 .6808 Mathlib/RingTheory/FiniteType.olean 574584 396736 .3095 Mathlib/Topology/Alexandroff.olean 396264 396264 .0000 Mathlib/Algebra/Hom/Equiv/TypeTags.olean 1167192 395776 .6609 Mathlib/RingTheory/WittVector/IsPoly.olean 1440736 395608 .7254 Mathlib/Data/MvPolynomial/Rename.olean 523856 395424 .2451 Mathlib/Topology/UnitInterval.olean 400520 394888 .0140 Mathlib/Data/Fin/Fin2.olean 545728 394680 .2767 Mathlib/CategoryTheory/Triangulated/Triangulated.olean 405680 394576 .0273 Mathlib/CategoryTheory/SingleObj.olean 614112 393864 .3586 Mathlib/Combinatorics/Young/YoungDiagram.olean 425320 391584 .0793 Mathlib/Algebra/Star/Unitary.olean 611344 391536 .3595 Mathlib/Init/Data/Nat/Bitwise.olean 708344 391448 .4473 Mathlib/Data/Real/Hyperreal.olean 390840 390840 .0000 Mathlib/Algebra/Category/ModuleCat/Tannaka.olean 978576 390824 .6006 Mathlib/RingTheory/Adjoin/Basic.olean 707256 390752 .4475 Mathlib/Analysis/InnerProductSpace/Spectrum.olean 395000 390704 .0108 Mathlib/CategoryTheory/Functor/Const.olean 426384 390096 .0851 Mathlib/Topology/Order/Hom/Basic.olean 468528 389832 .1679 Mathlib/Algebra/EuclideanDomain/Defs.olean 629544 389080 .3819 Mathlib/Analysis/Analytic/Linear.olean 392592 388192 .0112 Mathlib/Tactic/Zify.olean 1459344 387664 .7343 Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.olean 781744 387608 .5041 Mathlib/MeasureTheory/Measure/FiniteMeasure.olean 1115280 387584 .6524 Mathlib/Algebra/IndicatorFunction.olean 392792 387464 .0135 Mathlib/Data/Set/Semiring.olean 416680 387240 .0706 Mathlib/Analysis/Convex/Body.olean 448016 386968 .1362 Mathlib/Topology/ContinuousFunction/Units.olean 413832 386472 .0661 Mathlib/CategoryTheory/FullSubcategory.olean 837664 386256 .5388 Mathlib/Combinatorics/HalesJewett.olean 389872 384456 .0138 Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.olean 414168 384264 .0722 Mathlib/Algebra/Group/OrderSynonym.olean 504264 383544 .2393 Mathlib/Control/Fold.olean 385152 383304 .0047 Mathlib/Order/Category/BoolAlgCat.olean 382592 382592 .0000 Mathlib/Tactic/ByContra.olean 397104 381736 .0387 Mathlib/Order/Category/FinBddDistLatCat.olean 399416 381608 .0445 Mathlib/GroupTheory/GroupAction/Prod.olean 427736 380928 .1094 Mathlib/Control/Functor.olean 706952 379944 .4625 Mathlib/Data/Nat/ModEq.olean 551024 379896 .3105 Mathlib/Topology/LocallyConstant/Basic.olean 516048 379888 .2638 Mathlib/Data/Rat/NNRat.olean 681352 379592 .4428 Mathlib/Data/Nat/Factorial/Basic.olean 376400 376400 .0000 Mathlib/Control/Writer.olean 490080 376296 .2321 Mathlib/Topology/MetricSpace/Closeds.olean 483744 375016 .2247 Mathlib/Computability/Encoding.olean 380336 374664 .0149 Mathlib/CategoryTheory/Limits/ExactFunctor.olean 401208 374408 .0667 Mathlib/Order/Heyting/Regular.olean 415840 374408 .0996 Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.olean 376632 374048 .0068 Mathlib/Tactic/CategoryTheory/Reassoc.olean 373928 373928 .0000 Mathlib/CategoryTheory/Closed/Types.olean 683016 373400 .4533 Mathlib/Algebra/Homology/ShortExact/Preadditive.olean 421504 373064 .1149 Mathlib/Order/FixedPoints.olean 374296 372888 .0037 Mathlib/Algebra/Category/BoolRingCat.olean 2768048 372624 .8653 Mathlib/Analysis/Convex/Between.olean 373456 372504 .0025 Mathlib/RingTheory/Derivation/Lie.olean 375072 372488 .0068 Mathlib/Tactic/Reassoc.olean 539152 372168 .3097 Mathlib/CategoryTheory/Preadditive/Injective.olean 968360 371112 .6167 Mathlib/Algebra/Order/Field/Basic.olean 1129536 370112 .6723 Mathlib/MeasureTheory/Constructions/Prod/Basic.olean 493352 369864 .2503 Mathlib/Data/Sigma/Basic.olean 537200 369072 .3129 Mathlib/RingTheory/SimpleModule.olean 762008 366784 .5186 Mathlib/Data/Nat/Order/Basic.olean 393832 366496 .0694 Mathlib/Algebra/Module/Bimodule.olean 849032 366456 .5683 Mathlib/LinearAlgebra/Matrix/ZPow.olean 486864 366264 .2477 Mathlib/CategoryTheory/Functor/EpiMono.olean 371088 365936 .0138 Mathlib/Tactic/NormNum/IsCoprime.olean 886960 365584 .5878 Mathlib/RingTheory/Multiplicity.olean 515808 365408 .2915 Mathlib/Analysis/Asymptotics/Theta.olean 363544 363544 .0000 Mathlib/Tactic/FailIfNoProgress.olean 504112 363440 .2790 Mathlib/Data/MvPolynomial/Division.olean 434784 363392 .1642 Mathlib/Combinatorics/Quiver/Symmetric.olean 539552 363240 .3267 Mathlib/FieldTheory/KrullTopology.olean 379456 363192 .0428 Mathlib/Algebra/Hom/Equiv/Units/Basic.olean 384640 363112 .0559 Mathlib/Data/Matrix/DMatrix.olean 382400 363032 .0506 Mathlib/LinearAlgebra/FreeModule/IdealQuotient.olean 1356232 362488 .7327 Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.olean 364648 362352 .0062 Mathlib/CategoryTheory/Groupoid.olean 554600 361544 .3481 Mathlib/RingTheory/Localization/FractionRing.olean 599616 361528 .3970 Mathlib/LinearAlgebra/AffineSpace/Ordered.olean 363136 361168 .0054 Mathlib/CategoryTheory/Category/QuivCat.olean 536600 360608 .3279 Mathlib/Data/Pi/Algebra.olean 458760 359904 .2154 Mathlib/Algebra/Order/SMul.olean 481712 359752 .2531 Mathlib/Analysis/NormedSpace/BanachSteinhaus.olean 975144 359632 .6312 Mathlib/Data/Finset/LocallyFinite.olean 1084728 359480 .6685 Mathlib/Data/Set/Prod.olean 528968 359312 .3207 Mathlib/Data/PFunctor/Multivariate/W.olean 541736 359288 .3367 Mathlib/Order/SuccPred/LinearLocallyFinite.olean 359176 359176 .0000 Mathlib/Util/AddRelatedDecl.olean 717288 357632 .5014 Mathlib/Analysis/Complex/Isometry.olean 602624 357032 .4075 Mathlib/RingTheory/Ideal/Prod.olean 369976 356640 .0360 Mathlib/AlgebraicGeometry/SheafedSpace.olean 842536 356568 .5767 Mathlib/RingTheory/Ideal/Over.olean 359560 356088 .0096 Mathlib/CategoryTheory/Monoidal/Internal/Limits.olean 973920 355856 .6346 Mathlib/Combinatorics/Additive/SalemSpencer.olean 526656 355784 .3244 Mathlib/LinearAlgebra/QuadraticForm/Prod.olean 357600 355664 .0054 Mathlib/Algebra/Module/Hom.olean 505840 355176 .2978 Mathlib/Data/Finset/Sym.olean 454552 354752 .2195 Mathlib/Order/Closure.olean 419936 354280 .1563 Mathlib/Data/W/Basic.olean 567144 353488 .3767 Mathlib/RingTheory/Polynomial/Hermite/Basic.olean 620584 353408 .4305 Mathlib/Deprecated/Submonoid.olean 426608 353104 .1722 Mathlib/LinearAlgebra/ProjectiveSpace/Subspace.olean 549064 352360 .3582 Mathlib/Computability/Language.olean 528200 352200 .3332 Mathlib/CategoryTheory/Groupoid/FreeGroupoid.olean 498008 352120 .2929 Mathlib/MeasureTheory/Covering/VitaliFamily.olean 702336 351616 .4993 Mathlib/Order/Monotone/Basic.olean 626424 351584 .4387 Mathlib/Topology/ContinuousFunction/Polynomial.olean 565136 351536 .3779 Mathlib/Order/Disjoint.olean 1321848 351360 .7341 Mathlib/SetTheory/Cardinal/Cofinality.olean 522224 351352 .3272 Mathlib/RingTheory/Int/Basic.olean 738584 351320 .5243 Mathlib/FieldTheory/Finite/Polynomial.olean 1003616 351192 .6500 Mathlib/Topology/Bases.olean 350984 350984 .0000 Mathlib/Tactic/RunCmd.olean 471016 350872 .2550 Mathlib/Data/Multiset/Fintype.olean 786640 350464 .5544 Mathlib/Analysis/Calculus/FDeriv/Add.olean 496640 350200 .2948 Mathlib/Topology/Sheaves/Forget.olean 798032 349904 .5615 Mathlib/Algebra/GroupPower/Order.olean 349880 349880 .0000 Mathlib/Tactic/SwapVar.olean 415592 349760 .1584 Mathlib/Data/Semiquot.olean 349456 349456 .0000 Mathlib/Tactic/ApplyCongr.olean 398064 349216 .1227 Mathlib/LinearAlgebra/Matrix/Reindex.olean 352656 347256 .0153 Mathlib/Tactic/GCongr/ForwardAttr.olean 904912 346864 .6166 Mathlib/Geometry/Manifold/LocalInvariantProperties.olean 698888 346768 .5038 Mathlib/Topology/Paracompact.olean 371768 345872 .0696 Mathlib/Analysis/Complex/UnitDisc/Basic.olean 365280 345776 .0533 Mathlib/Order/Category/BddDistLatCat.olean 721952 345392 .5215 Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.olean 719480 344496 .5211 Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.olean 400936 344224 .1414 Mathlib/Algebra/Category/ModuleCat/Subobject.olean 1609320 343840 .7863 Mathlib/Data/Polynomial/Derivative.olean 913984 343528 .6241 Mathlib/RingTheory/WittVector/WittPolynomial.olean 562880 343232 .3902 Mathlib/Analysis/Calculus/FDeriv/Bilinear.olean 630704 343184 .4558 Mathlib/Analysis/SpecialFunctions/PolarCoord.olean 384784 343120 .1082 Mathlib/MeasureTheory/Function/LpOrder.olean 1108392 342656 .6908 Mathlib/Topology/UniformSpace/UniformConvergence.olean 486304 342520 .2956 Mathlib/Combinatorics/Additive/Etransform.olean 359512 342344 .0477 Mathlib/Order/Category/BddOrdCat.olean 604488 341472 .4351 Mathlib/Order/Cover.olean 753248 341128 .5471 Mathlib/Order/Filter/NAry.olean 510504 340480 .3330 Mathlib/Control/Functor/Multivariate.olean 610312 339336 .4439 Mathlib/GroupTheory/Finiteness.olean 344288 339224 .0147 Mathlib/Algebra/Order/Monoid/Cancel/Defs.olean 850568 339128 .6012 Mathlib/GroupTheory/Index.olean 804880 338424 .5795 Mathlib/Data/Finset/Card.olean 403416 337336 .1638 Mathlib/AlgebraicTopology/DoldKan/Normalized.olean 819336 336528 .5892 Mathlib/RingTheory/Polynomial/Dickson.olean 685216 336000 .5096 Mathlib/Dynamics/OmegaLimit.olean 420048 335968 .2001 Mathlib/LinearAlgebra/AffineSpace/Restrict.olean 814352 335320 .5882 Mathlib/Geometry/Euclidean/Angle/Sphere.olean 464776 334464 .2803 Mathlib/SetTheory/Ordinal/NaturalOps.olean 358576 334424 .0673 Mathlib/Data/Vector.olean 377768 334312 .1150 Mathlib/CategoryTheory/Idempotents/Biproducts.olean 340776 333368 .0217 Mathlib/GroupTheory/GroupAction/Units.olean 742688 333264 .5512 Mathlib/Data/List/Pairwise.olean 491304 332848 .3225 Mathlib/CategoryTheory/CommSq.olean 1121416 332768 .7032 Mathlib/FieldTheory/Finite/Basic.olean 668136 332224 .5027 Mathlib/Algebra/Periodic.olean 370128 332160 .1025 Mathlib/Algebra/Category/ModuleCat/Images.olean 340096 332056 .0236 Mathlib/RingTheory/RingInvo.olean 663432 331888 .4997 Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.olean 424632 331648 .2189 Mathlib/Topology/Algebra/UniformField.olean 589176 331616 .4371 Mathlib/Combinatorics/SetFamily/Shadow.olean 591632 329960 .4422 Mathlib/Data/QPF/Multivariate/Constructions/Fix.olean 462352 328416 .2896 Mathlib/Analysis/BoxIntegral/Partition/Tagged.olean 606472 328072 .4590 Mathlib/Analysis/Calculus/Deriv/Basic.olean 1835272 327680 .8214 Mathlib/Analysis/Convex/Combination.olean 444368 326584 .2650 Mathlib/RingTheory/WittVector/Teichmuller.olean 375320 326384 .1303 Mathlib/Algebra/ContinuedFractions/Basic.olean 429752 325688 .2421 Mathlib/Topology/DiscreteQuotient.olean 1257536 325136 .7414 Mathlib/Analysis/Calculus/Deriv/Mul.olean 325904 324936 .0029 Mathlib/Order/LatticeIntervals.olean 382168 324752 .1502 Mathlib/Data/Fintype/Quotient.olean 538128 324288 .3973 Mathlib/Data/String/Basic.olean 538648 324040 .3984 Mathlib/Topology/Algebra/Order/Compact.olean 483008 323864 .3294 Mathlib/RingTheory/LaurentSeries.olean 534784 323720 .3946 Mathlib/Data/Fin/Tuple/NatAntidiagonal.olean 431760 323168 .2515 Mathlib/Analysis/NormedSpace/Extend.olean 322920 322920 .0000 Mathlib.olean 760416 322656 .5756 Mathlib/CategoryTheory/Sites/Coverage.olean 381008 321784 .1554 Mathlib/CategoryTheory/EpiMono.olean 324000 321696 .0071 Mathlib/CategoryTheory/Monoidal/Functorial.olean 381672 321008 .1589 Mathlib/MeasureTheory/Integral/IntervalAverage.olean 787264 320736 .5925 Mathlib/Data/List/Nodup.olean 367352 320272 .1281 Mathlib/CategoryTheory/Limits/ColimitLimit.olean 817160 320272 .6080 Mathlib/Algebra/CharP/Basic.olean 1243416 319864 .7427 Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.olean 554400 319440 .4238 Mathlib/Data/Finset/Powerset.olean 706824 319176 .5484 Mathlib/Data/List/MinMax.olean 320096 318968 .0035 Mathlib/CategoryTheory/Core.olean 822488 318504 .6127 Mathlib/Algebra/BigOperators/Multiset/Basic.olean 317592 317592 .0000 Mathlib/Tactic/Monotonicity/Basic.olean 931104 317464 .6590 Mathlib/NumberTheory/WellApproximable.olean 321184 316952 .0131 Mathlib/Analysis/NormedSpace/Completion.olean 315816 315816 .0000 Mathlib/Lean/Name.olean 321880 315008 .0213 Mathlib/MeasureTheory/Measure/Lebesgue/Complex.olean 765432 314848 .5886 Mathlib/Data/Polynomial/Coeff.olean 514520 314504 .3887 Mathlib/Data/Int/Order/Basic.olean 355912 314360 .1167 Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.olean 773536 314168 .5938 Mathlib/Algebra/BigOperators/Order.olean 414224 314104 .2417 Mathlib/Data/Finsupp/Order.olean 658424 314096 .5229 Mathlib/Algebra/Order/Archimedean.olean 686360 313680 .5429 Mathlib/Data/Nat/Prime.olean 568736 313576 .4486 Mathlib/Order/CountableDenseLinearOrder.olean 588632 313064 .4681 Mathlib/RingTheory/MvPolynomial/Symmetric.olean 1236984 313056 .7469 Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.olean 769872 312808 .5936 Mathlib/RingTheory/PrincipalIdealDomain.olean 838464 312080 .6277 Mathlib/FieldTheory/Minpoly/Field.olean 314720 311952 .0087 Mathlib/Tactic/NoncommRing.olean 859328 311904 .6370 Mathlib/MeasureTheory/Integral/IntegralEqImproper.olean 311880 311880 .0000 Mathlib/Algebra/Order/Field/Defs.olean 312816 311432 .0044 Mathlib/Algebra/Order/Monoid/OrderDual.olean 311408 311408 .0000 Mathlib/Tactic/Rename.olean 622928 311232 .5003 Mathlib/Analysis/NormedSpace/Star/GelfandDuality.olean 706728 310816 .5602 Mathlib/Algebra/Jordan/Basic.olean 580104 310664 .4644 Mathlib/Data/Rat/Defs.olean 429208 310656 .2762 Mathlib/CategoryTheory/Preadditive/Projective.olean 790672 310472 .6073 Mathlib/RingTheory/JacobsonIdeal.olean 1347496 310320 .7697 Mathlib/RingTheory/Localization/Integral.olean 1105480 307872 .7215 Mathlib/Data/Finset/NoncommProd.olean 338400 307184 .0922 Mathlib/Topology/Hom/Open.olean 1160304 306752 .7356 Mathlib/LinearAlgebra/Trace.olean 759728 306400 .5966 Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.olean 312952 306312 .0212 Mathlib/Topology/MetricSpace/Algebra.olean 338160 306160 .0946 Mathlib/Topology/Algebra/Module/Star.olean 622920 305800 .5090 Mathlib/Data/Set/Intervals/UnorderedInterval.olean 330344 305712 .0745 Mathlib/Data/Fintype/Option.olean 2006688 304936 .8480 Mathlib/MeasureTheory/Function/Jacobian.olean 435912 304056 .3024 Mathlib/Combinatorics/SetFamily/Compression/Down.olean 645784 304000 .5292 Mathlib/ModelTheory/Definability.olean 775144 303768 .6081 Mathlib/Combinatorics/SetFamily/Compression/UV.olean 676392 303656 .5510 Mathlib/MeasureTheory/Measure/Haar/OfBasis.olean 1025776 303520 .7041 Mathlib/Data/Set/Ncard.olean 303192 303192 .0000 Mathlib/Tactic/Replace.olean 933664 302824 .6756 Mathlib/RingTheory/PolynomialAlgebra.olean 709464 302808 .5731 Mathlib/Topology/MetricSpace/GromovHausdorffRealized.olean 315136 302392 .0404 Mathlib/Data/LazyList.olean 1040816 301704 .7101 Mathlib/Analysis/SpecialFunctions/Gamma/Basic.olean 301384 301384 .0000 Mathlib/Tactic/Spread.olean 302024 301320 .0023 Mathlib/Data/Matrix/DualNumber.olean 526712 300936 .4286 Mathlib/Algebra/Lie/Normalizer.olean 426864 300616 .2957 Mathlib/Data/Set/Sups.olean 671848 300448 .5528 Mathlib/RingTheory/Localization/Away/Basic.olean 910360 299928 .6705 Mathlib/Data/Nat/Digits.olean 405720 299560 .2616 Mathlib/Algebra/MonoidAlgebra/Division.olean 299544 299544 .0000 Mathlib/Control/Random.olean 449264 299512 .3333 Mathlib/Data/Prod/TProd.olean 299440 299440 .0000 Mathlib/CategoryTheory/Limits/Preserves/Finite.olean 368736 298992 .1891 Mathlib/Topology/Algebra/WithZeroTopology.olean 955344 298976 .6870 Mathlib/MeasureTheory/Decomposition/Jordan.olean 1198744 298624 .7508 Mathlib/Analysis/Complex/PhragmenLindelof.olean 337424 298448 .1155 Mathlib/Data/W/Constructions.olean 336080 297672 .1142 Mathlib/CategoryTheory/Category/Pointed.olean 717112 297672 .5849 Mathlib/CategoryTheory/Sites/CoverPreserving.olean 718688 297664 .5858 Mathlib/Topology/Semicontinuous.olean 725752 296384 .5916 Mathlib/MeasureTheory/Integral/IntegrableOn.olean 442656 296144 .3309 Mathlib/Analysis/Convex/SimplicialComplex/Basic.olean 512536 295456 .4235 Mathlib/Analysis/NormedSpace/TrivSqZeroExt.olean 312104 295272 .0539 Mathlib/Algebra/Algebra/RestrictScalars.olean 491016 295144 .3989 Mathlib/LinearAlgebra/Matrix/PosDef.olean 318280 294920 .0733 Mathlib/CategoryTheory/ConcreteCategory/Basic.olean 299776 294752 .0167 Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.olean 1060552 294704 .7221 Mathlib/Analysis/Convex/Basic.olean 404440 294328 .2722 Mathlib/Data/PNat/Basic.olean 448136 294288 .3433 Mathlib/Deprecated/Group.olean 791016 292576 .6301 Mathlib/Algebra/Order/LatticeGroup.olean 486496 292512 .3987 Mathlib/Algebra/ModEq.olean 292408 292408 .0000 Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.olean 292288 292288 .0000 Mathlib/Data/ListM/Split.olean 311840 292048 .0634 Mathlib/Control/Bifunctor.olean 295544 291984 .0120 Mathlib/Testing/SlimCheck/Gen.olean 720744 291864 .5950 Mathlib/ModelTheory/Satisfiability.olean 336744 291728 .1336 Mathlib/Control/Traversable/Basic.olean 292000 291200 .0027 Mathlib/Algebra/GroupRingAction/Invariant.olean 360304 290704 .1931 Mathlib/Algebra/Algebra/Subalgebra/Tower.olean 578872 289976 .4990 Mathlib/Computability/Ackermann.olean 422424 289952 .3136 Mathlib/Order/Antichain.olean 347912 289888 .1667 Mathlib/CategoryTheory/Shift/CommShift.olean 538000 289824 .4612 Mathlib/Combinatorics/SimpleGraph/Clique.olean 295280 289696 .0189 Mathlib/Algebra/Order/Monoid/TypeTags.olean 294800 289464 .0181 Mathlib/Data/Bundle.olean 593440 288688 .5135 Mathlib/Topology/ShrinkingLemma.olean 301104 288424 .0421 Mathlib/Logic/Embedding/Set.olean 745864 288336 .6134 Mathlib/Data/List/Indexes.olean 476616 287928 .3958 Mathlib/Analysis/NormedSpace/MazurUlam.olean 978776 287656 .7061 Mathlib/RingTheory/Polynomial/Content.olean 296064 287624 .0285 Mathlib/GroupTheory/PresentedGroup.olean 825408 287288 .6519 Mathlib/AlgebraicGeometry/Stalks.olean 525680 286624 .4547 Mathlib/GroupTheory/Subgroup/Finite.olean 286576 286576 .0000 Mathlib/Tactic/PermuteGoals.olean 289576 286360 .0111 Mathlib/CategoryTheory/Linear/LinearFunctor.olean 331784 286288 .1371 Mathlib/CategoryTheory/NatTrans.olean 575632 285976 .5031 Mathlib/Order/Filter/Lift.olean 470536 285776 .3926 Mathlib/Analysis/Calculus/FDeriv/Prod.olean 286432 285256 .0041 Mathlib/Order/Category/HeytAlgCat.olean 643120 284688 .5573 Mathlib/Topology/MetricSpace/Lipschitz.olean 541864 284296 .4753 Mathlib/CategoryTheory/Limits/Shapes/KernelPair.olean 283552 283552 .0000 Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.olean 287440 283432 .0139 Mathlib/Data/QPF/Multivariate/Constructions/Sigma.olean 287760 283032 .0164 Mathlib/CategoryTheory/Limits/Pi.olean 423472 282896 .3319 Mathlib/Topology/MetricSpace/Polish.olean 302848 282552 .0670 Mathlib/MeasureTheory/Group/MeasurableEquiv.olean 305336 282096 .0761 Mathlib/Topology/ContinuousFunction/Ordered.olean 717520 279856 .6099 Mathlib/Data/PNat/Xgcd.olean 390264 279824 .2829 Mathlib/Data/Sigma/Lex.olean 1308392 279704 .7862 Mathlib/FieldTheory/Separable.olean 636696 279624 .5608 Mathlib/Algebra/GroupPower/Basic.olean 279472 279472 .0000 Mathlib/Util/PiNotation.olean 569808 278464 .5113 Mathlib/Topology/Maps.olean 283736 277904 .0205 Mathlib/CategoryTheory/Category/Grpd.olean 957848 277672 .7101 Mathlib/Analysis/SpecialFunctions/Pow/NNReal.olean 532936 277320 .4796 Mathlib/CategoryTheory/EqToHom.olean 794336 277256 .6509 Mathlib/MeasureTheory/Group/Prod.olean 310816 276840 .1093 Mathlib/Data/Polynomial/Degree/CardPowDegree.olean 285064 276536 .0299 Mathlib/GroupTheory/IsFreeGroup.olean 389696 274328 .2960 Mathlib/Data/Finset/Sort.olean 451544 273336 .3946 Mathlib/LinearAlgebra/Matrix/Hermitian.olean 274472 273184 .0046 Mathlib/Order/Category/LatCat.olean 322696 272888 .1543 Mathlib/Dynamics/Flow.olean 275608 272824 .0101 Mathlib/Algebra/Order/Monoid/Cancel/Basic.olean 960616 272776 .7160 Mathlib/Analysis/InnerProductSpace/Rayleigh.olean 999048 272280 .7274 Mathlib/GroupTheory/Perm/Support.olean 426920 272224 .3623 Mathlib/Order/Directed.olean 365904 272008 .2566 Mathlib/Probability/ConditionalProbability.olean 663128 271920 .5899 Mathlib/Data/Rat/Cast.olean 644120 271824 .5779 Mathlib/GroupTheory/SpecificGroups/Alternating.olean 885512 271656 .6932 Mathlib/LinearAlgebra/StdBasis.olean 372568 271640 .2708 Mathlib/Data/Rel.olean 1492880 271480 .8181 Mathlib/Analysis/Calculus/FDerivMeasurable.olean 563824 271000 .5193 Mathlib/Algebra/Support.olean 290944 270944 .0687 Mathlib/MeasureTheory/Measure/Complex.olean 273000 270904 .0076 Mathlib/Algebra/Module/Pi.olean 786104 270816 .6554 Mathlib/Algebra/BigOperators/Intervals.olean 311120 270776 .1296 Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.olean 289824 270616 .0662 Mathlib/Data/PNat/Defs.olean 632440 270560 .5721 Mathlib/Data/Nat/Bitwise.olean 278280 270384 .0283 Mathlib/LinearAlgebra/QuadraticForm/Complex.olean 701872 270176 .6150 Mathlib/Combinatorics/SimpleGraph/Density.olean 542408 269936 .5023 Mathlib/Data/Nat/Choose/Basic.olean 418752 269824 .3556 Mathlib/Control/Applicative.olean 277488 268936 .0308 Mathlib/Tactic/Qify.olean 280280 268616 .0416 Mathlib/LinearAlgebra/QuadraticForm/Real.olean 269000 267824 .0043 Mathlib/Algebra/Category/GroupWithZeroCat.olean 288248 267640 .0714 Mathlib/Topology/Category/UniformSpace.olean 335112 267512 .2017 Mathlib/Algebra/Order/Ring/Canonical.olean 685280 267096 .6102 Mathlib/GroupTheory/Transfer.olean 269624 266760 .0106 Mathlib/CategoryTheory/Monad/Types.olean 627488 266720 .5749 Mathlib/Data/Finset/NAry.olean 634688 266280 .5804 Mathlib/LinearAlgebra/Finrank.olean 697816 266128 .6186 Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.olean 293128 265984 .0926 Mathlib/Algebra/Order/Monoid/WithZero/Defs.olean 265952 265952 .0000 Mathlib/Tactic/SuccessIfFailWithMsg.olean 576184 265568 .5390 Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.olean 868592 265416 .6944 Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.olean 277968 265096 .0463 Mathlib/Data/Fintype/Order.olean 348232 264960 .2391 Mathlib/Analysis/NormedSpace/Complemented.olean 830000 264720 .6810 Mathlib/RingTheory/Artinian.olean 966248 264464 .7262 Mathlib/MeasureTheory/Measure/Lebesgue/Basic.olean 691976 263888 .6186 Mathlib/Topology/Algebra/UniformConvergence.olean 787848 263768 .6652 Mathlib/Order/WellFoundedSet.olean 622736 263728 .5765 Mathlib/MeasureTheory/Measure/Content.olean 309496 263512 .1485 Mathlib/CategoryTheory/EssentiallySmall.olean 907136 260760 .7125 Mathlib/MeasureTheory/Covering/Vitali.olean 261944 260728 .0046 Mathlib/Order/Category/CompleteLatCat.olean 395720 260640 .3413 Mathlib/Algebra/Group/Commute.olean 616440 260488 .5774 Mathlib/Topology/MetricSpace/MetrizableUniformity.olean 334224 260464 .2206 Mathlib/Combinatorics/Derangements/Basic.olean 477784 259928 .4559 Mathlib/Algebra/Category/GroupCat/Injective.olean 272536 259808 .0467 Mathlib/Data/Finsupp/Lex.olean 764264 259808 .6600 Mathlib/MeasureTheory/Measure/Stieltjes.olean 500800 259664 .4815 Mathlib/Topology/Instances/Matrix.olean 379368 259360 .3163 Mathlib/RingTheory/ReesAlgebra.olean 420648 259016 .3842 Mathlib/Data/Nat/Cast/Basic.olean 343448 258888 .2462 Mathlib/Data/Nat/Cast/Defs.olean 265040 258408 .0250 Mathlib/Algebra/Star/Free.olean 349224 258136 .2608 Mathlib/CategoryTheory/Sites/Types.olean 616992 257984 .5818 Mathlib/Data/Nat/Squarefree.olean 257752 257752 .0000 Mathlib/Data/Int/Cast/Defs.olean 1006616 257352 .7443 Mathlib/Combinatorics/Additive/Behrend.olean 354752 257264 .2748 Mathlib/Data/List/Duplicate.olean 574992 256776 .5534 Mathlib/Analysis/NormedSpace/AddTorsor.olean 273432 256368 .0624 Mathlib/Data/Sigma/Interval.olean 415984 256368 .3837 Mathlib/Algebra/Polynomial/GroupRingAction.olean 879432 256352 .7085 Mathlib/MeasureTheory/Function/AEEqOfIntegral.olean 485664 256320 .4722 Mathlib/Analysis/LocallyConvex/WeakDual.olean 407928 256272 .3717 Mathlib/Data/Fin/Tuple/Sort.olean 767896 256208 .6663 Mathlib/Probability/Martingale/Basic.olean 258408 256168 .0086 Mathlib/CategoryTheory/FinCategory.olean 474456 256144 .4601 Mathlib/Data/Rat/Order.olean 256024 256024 .0000 Mathlib/Data/ListM/IO.olean 328664 255760 .2218 Mathlib/CategoryTheory/PUnit.olean 255752 255752 .0000 Mathlib/Tactic/InferParam.olean 306632 255752 .1659 Mathlib/CategoryTheory/Conj.olean 650856 255144 .6079 Mathlib/Analysis/Calculus/IteratedDeriv.olean 258648 254640 .0154 Mathlib/Algebra/Order/Group/InjSurj.olean 378072 254552 .3267 Mathlib/MeasureTheory/Function/SimpleFuncDense.olean 276152 254488 .0784 Mathlib/GroupTheory/Commensurable.olean 254392 254392 .0000 Mathlib/Util/LongNames.olean 378912 254392 .3286 Mathlib/LinearAlgebra/Matrix/LDL.olean 255688 254176 .0059 Mathlib/Order/Category/PreordCat.olean 320688 254064 .2077 Mathlib/ModelTheory/Order.olean 1881336 253448 .8652 Mathlib/RingTheory/LocalProperties.olean 593688 253368 .5732 Mathlib/Probability/ProbabilityMassFunction/Monad.olean 253312 252184 .0044 Mathlib/Order/Category/FrmCat.olean 252744 252104 .0025 Mathlib/Algebra/Ring/Aut.olean 260984 251720 .0354 Mathlib/Tactic/NormNum/NatSqrt.olean 1036712 251416 .7574 Mathlib/Analysis/SpecialFunctions/Pow/Deriv.olean 252520 251328 .0047 Mathlib/Order/Category/LinOrdCat.olean 438216 251088 .4270 Mathlib/RingTheory/Adjoin/Field.olean 613224 250944 .5907 Mathlib/CategoryTheory/Abelian/LeftDerived.olean 944032 250920 .7342 Mathlib/Analysis/Convex/Gauge.olean 1185856 250816 .7884 Mathlib/Probability/Independence/Basic.olean 249968 249968 .0000 Mathlib/Tactic/Classical.olean 281312 249904 .1116 Mathlib/Algebra/Order/Ring/Cone.olean 367296 249536 .3206 Mathlib/AlgebraicTopology/DoldKan/GammaCompN.olean 807104 249496 .6908 Mathlib/Algebra/Module/Zlattice.olean 404448 248936 .3845 Mathlib/Combinatorics/SimpleGraph/Coloring.olean 283568 248736 .1228 Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.olean 391584 248480 .3654 Mathlib/Data/Bitvec/Lemmas.olean 288992 248440 .1403 Mathlib/Topology/ContinuousFunction/CocompactMap.olean 479176 248384 .4816 Mathlib/Analysis/InnerProductSpace/Positive.olean 416824 247464 .4063 Mathlib/MeasureTheory/Measure/NullMeasurable.olean 517056 247328 .5216 Mathlib/Data/Int/Log.olean 932328 247080 .7349 Mathlib/MeasureTheory/Integral/VitaliCaratheodory.olean 416664 246896 .4074 Mathlib/Algebra/BigOperators/Associated.olean 632328 246248 .6105 Mathlib/Data/List/NodupEquivFin.olean 368848 246176 .3325 Mathlib/Combinatorics/Hall/Basic.olean 320464 245040 .2353 Mathlib/Data/Matrix/Reflection.olean 446968 244200 .4536 Mathlib/CategoryTheory/Sites/Surjective.olean 410728 244024 .4058 Mathlib/Topology/Algebra/Order/MonotoneConvergence.olean 265152 243696 .0809 Mathlib/ModelTheory/Bundled.olean 405816 243624 .3996 Mathlib/Data/Set/Pointwise/Finite.olean 416584 242736 .4173 Mathlib/Data/Sum/Interval.olean 242728 242728 .0000 Mathlib/Topology/Category/Profinite/AsLimit.olean 245440 242696 .0111 Mathlib/Topology/ContinuousFunction/LocallyConstant.olean 408848 242616 .4065 Mathlib/MeasureTheory/Group/Action.olean 255840 242456 .0523 Mathlib/Topology/Algebra/UniformMulAction.olean 928400 242272 .7390 Mathlib/Probability/Martingale/Upcrossing.olean 308816 242224 .2156 Mathlib/Algebra/Star/Order.olean 782080 241616 .6910 Mathlib/Algebra/Star/CHSH.olean 426664 241560 .4338 Mathlib/Data/Int/ModEq.olean 241240 241240 .0000 Mathlib/Tactic/RenameBVar.olean 272512 241048 .1154 Mathlib/Data/Dfinsupp/Multiset.olean 604208 241048 .6010 Mathlib/Topology/Algebra/Order/LiminfLimsup.olean 617208 241024 .6094 Mathlib/Topology/Algebra/Order/IntermediateValue.olean 599168 241008 .5977 Mathlib/GroupTheory/SchurZassenhaus.olean 446472 240208 .4619 Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.olean 547104 239600 .5620 Mathlib/Combinatorics/SimpleGraph/AdjMatrix.olean 252192 239520 .0502 Mathlib/GroupTheory/GroupAction/Sigma.olean 569040 238472 .5809 Mathlib/Algebra/Parity.olean 457072 237760 .4798 Mathlib/AlgebraicTopology/DoldKan/Projections.olean 259936 237688 .0855 Mathlib/Init/Function.olean 751344 237320 .6841 Mathlib/Order/CompactlyGenerated.olean 473952 236696 .5005 Mathlib/Data/List/Lattice.olean 292944 236352 .1931 Mathlib/Data/Fin/Tuple/Reflection.olean 792224 236224 .7018 Mathlib/Analysis/SpecialFunctions/Exponential.olean 1058120 236072 .7768 Mathlib/Analysis/MeanInequalities.olean 805000 235944 .7069 Mathlib/Analysis/Convex/Strict.olean 338768 235344 .3052 Mathlib/RingTheory/Localization/AsSubring.olean 485048 235136 .5152 Mathlib/RingTheory/MvPolynomial/Homogeneous.olean 694256 234752 .6618 Mathlib/Analysis/InnerProductSpace/Symmetric.olean 235760 234440 .0055 Mathlib/Order/Category/DistLatCat.olean 608672 233680 .6160 Mathlib/MeasureTheory/Integral/Periodic.olean 373632 233480 .3751 Mathlib/Data/PFunctor/Multivariate/Basic.olean 382248 233288 .3896 Mathlib/Order/Filter/Extr.olean 537112 232984 .5662 Mathlib/Data/Int/GCD.olean 235536 232384 .0133 Mathlib/Combinatorics/Quiver/Arborescence.olean 591160 232040 .6074 Mathlib/Analysis/Complex/AbsMax.olean 314880 231952 .2633 Mathlib/Analysis/Normed/Order/Lattice.olean 719928 231912 .6778 Mathlib/CategoryTheory/MorphismProperty.olean 394872 231824 .4129 Mathlib/Combinatorics/SimpleGraph/Ends/Defs.olean 791152 231768 .7070 Mathlib/Data/Set/NAry.olean 495464 231680 .5323 Mathlib/Deprecated/Subring.olean 389936 231648 .4059 Mathlib/CategoryTheory/Functor/LeftDerived.olean 270120 231520 .1428 Mathlib/Data/ENat/Basic.olean 341784 231352 .3231 Mathlib/RingTheory/NonZeroDivisors.olean 231432 230976 .0019 Mathlib/Algebra/Category/Ring/Adjunctions.olean 1070352 230752 .7844 Mathlib/Probability/Kernel/CondCdf.olean 398752 230680 .4214 Mathlib/Control/LawfulFix.olean 230472 230472 .0000 Mathlib/CategoryTheory/Bicategory/End.olean 579024 230416 .6020 Mathlib/FieldTheory/ChevalleyWarning.olean 366096 230168 .3712 Mathlib/Data/Dfinsupp/NeLocus.olean 230024 230024 .0000 Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.olean 477584 229616 .5192 Mathlib/RingTheory/WittVector/MulP.olean 272912 229592 .1587 Mathlib/Data/Nat/Factorial/DoubleFactorial.olean 349056 229432 .3427 Mathlib/GroupTheory/FreeAbelianGroupFinsupp.olean 349776 229400 .3441 Mathlib/GroupTheory/Subgroup/ZPowers.olean 403720 229232 .4322 Mathlib/Data/Nat/Order/Lemmas.olean 240080 229096 .0457 Mathlib/AlgebraicTopology/TopologicalSimplex.olean 229048 229048 .0000 Mathlib/Tactic/Explode/Pretty.olean 723232 228840 .6835 Mathlib/MeasureTheory/Measure/Regular.olean 241704 228688 .0538 Mathlib/Data/Erased.olean 393312 228432 .4192 Mathlib/CategoryTheory/Sites/Closed.olean 447848 228248 .4903 Mathlib/Algebra/Order/Sub/Canonical.olean 976928 227368 .7672 Mathlib/Algebra/GeomSum.olean 230528 227296 .0140 Mathlib/CategoryTheory/Groupoid/VertexGroup.olean 307960 226480 .2645 Mathlib/Topology/Bornology/Basic.olean 353720 226392 .3599 Mathlib/RepresentationTheory/Maschke.olean 667968 226104 .6615 Mathlib/Order/SupIndep.olean 384376 225896 .4123 Mathlib/Algebra/CharP/MixedCharZero.olean 225800 225800 .0000 Mathlib/Tactic/Inhabit.olean 590000 225720 .6174 Mathlib/Analysis/Convex/StrictConvexSpace.olean 723128 225520 .6881 Mathlib/Probability/Kernel/IntegralCompProd.olean 473696 225416 .5241 Mathlib/Data/Sym/Card.olean 473232 225176 .5241 Mathlib/CategoryTheory/Abelian/Transfer.olean 575456 224992 .6090 Mathlib/Algebra/Homology/Exact.olean 641776 224960 .6494 Mathlib/Data/List/Count.olean 343352 224848 .3451 Mathlib/Topology/Order/LowerTopology.olean 437408 224528 .4866 Mathlib/ModelTheory/Ultraproducts.olean 313800 224464 .2846 Mathlib/Topology/Algebra/Field.olean 224056 224056 .0000 Mathlib/Algebra/Category/GroupCat/ZModuleEquivalence.olean 230440 223856 .0285 Mathlib/CategoryTheory/Category/Preorder.olean 539152 223800 .5849 Mathlib/FieldTheory/SplittingField/IsSplittingField.olean 397088 223712 .4366 Mathlib/MeasureTheory/Measure/ProbabilityMeasure.olean 248312 223056 .1017 Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.olean 601736 222712 .6298 Mathlib/MeasureTheory/Function/LocallyIntegrable.olean 223672 222480 .0053 Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.olean 236856 222352 .0612 Mathlib/Util/AtomM.olean 297448 222288 .2526 Mathlib/CategoryTheory/Abelian/FunctorCategory.olean 243920 222240 .0888 Mathlib/CategoryTheory/FintypeCat.olean 233032 222144 .0467 Mathlib/Tactic/Measurability.olean 564536 221816 .6070 Mathlib/Data/Finset/Prod.olean 1017512 221648 .7821 Mathlib/MeasureTheory/Constructions/Polish.olean 226808 221592 .0229 Mathlib/Algebra/Order/Monoid/Basic.olean 382768 221440 .4214 Mathlib/CategoryTheory/Preadditive/Schur.olean 451568 221392 .5097 Mathlib/Analysis/NormedSpace/Star/Mul.olean 275184 221160 .1963 Mathlib/Algebra/CovariantAndContravariant.olean 373064 221136 .4072 Mathlib/RingTheory/Localization/AtPrime.olean 223824 220928 .0129 Mathlib/CategoryTheory/Sites/Pushforward.olean 272704 220808 .1903 Mathlib/CategoryTheory/Preadditive/InjectiveResolution.olean 243872 220664 .0951 Mathlib/Data/Finsupp/Pointwise.olean 542312 220536 .5933 Mathlib/Analysis/Calculus/Deriv/Comp.olean 326560 220448 .3249 Mathlib/Topology/LocalExtr.olean 225848 220160 .0251 Mathlib/CategoryTheory/Preadditive/Opposite.olean 258888 220144 .1496 Mathlib/Topology/Spectral/Hom.olean 220248 220056 .0008 Mathlib/MeasureTheory/Category/MeasCat.olean 437720 220016 .4973 Mathlib/Data/Int/Cast/Lemmas.olean 268328 219976 .1801 Mathlib/Order/Filter/ZeroAndBoundedAtFilter.olean 260816 219056 .1601 Mathlib/Data/Int/Basic.olean 225088 219024 .0269 Mathlib/Algebra/GradedMulAction.olean 385168 218672 .4322 Mathlib/Control/Traversable/Instances.olean 351232 218616 .3775 Mathlib/Algebra/GroupWithZero/Basic.olean 269208 218032 .1900 Mathlib/Algebra/Star/Pointwise.olean 341984 217984 .3625 Mathlib/CategoryTheory/Preadditive/OfBiproducts.olean 238128 217968 .0846 Mathlib/Algebra/Category/ModuleCat/Products.olean 217912 217912 .0000 Mathlib/Algebra/Abs.olean 399480 217904 .4545 Mathlib/Data/Option/Basic.olean 495616 217720 .5607 Mathlib/Analysis/NormedSpace/Units.olean 1493992 217696 .8542 Mathlib/Analysis/SpecialFunctions/Integrals.olean 218936 217376 .0071 Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.olean 241768 217296 .1012 Mathlib/GroupTheory/EckmannHilton.olean 1483160 217224 .8535 Mathlib/MeasureTheory/Function/UniformIntegrable.olean 493480 217048 .5601 Mathlib/Data/Multiset/Bind.olean 379056 216952 .4276 Mathlib/Order/Compare.olean 598944 216888 .6378 Mathlib/Data/Set/Pointwise/Interval.olean 231288 216592 .0635 Mathlib/Data/Option/Defs.olean 566344 216368 .6179 Mathlib/Algebra/EuclideanDomain/Basic.olean 515168 215712 .5812 Mathlib/Algebra/Module/Submodule/Bilinear.olean 894072 215584 .7588 Mathlib/RingTheory/Localization/LocalizationLocalization.olean 594344 215448 .6375 Mathlib/Data/Real/GoldenRatio.olean 532152 215160 .5956 Mathlib/Data/List/OfFn.olean 977792 214744 .7803 Mathlib/Analysis/Calculus/TangentCone.olean 354360 214672 .3941 Mathlib/Analysis/Complex/Liouville.olean 538144 214608 .6012 Mathlib/Algebra/Group/UniqueProds.olean 275048 214344 .2207 Mathlib/CategoryTheory/Limits/Preserves/Limits.olean 214136 213848 .0013 Mathlib/Topology/Category/TopCat/Adjunctions.olean 262672 213816 .1859 Mathlib/Combinatorics/Partition.olean 238264 213456 .1041 Mathlib/Data/ByteArray.olean 387912 213280 .4501 Mathlib/Data/Bool/Basic.olean 214208 213256 .0044 Mathlib/Data/Set/Intervals/IsoIoo.olean 239208 213256 .1084 Mathlib/CategoryTheory/Category/TwoP.olean 324024 213256 .3418 Mathlib/Topology/MetricSpace/Baire.olean 213824 213128 .0032 Mathlib/Tactic/Contrapose.olean 461488 213096 .5382 Mathlib/Order/Filter/Pi.olean 217656 213072 .0210 Mathlib/GroupTheory/GroupAction/Opposite.olean 590312 212912 .6393 Mathlib/MeasureTheory/Function/ConvergenceInMeasure.olean 352760 212680 .3970 Mathlib/Data/PFunctor/Univariate/Basic.olean 419016 212616 .4925 Mathlib/Topology/Sequences.olean 462472 212520 .5404 Mathlib/Combinatorics/Hindman.olean 227944 211432 .0724 Mathlib/Topology/Instances/RatLemmas.olean 576776 211432 .6334 Mathlib/Algebra/Homology/QuasiIso.olean 235320 211416 .1015 Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.olean 926408 211000 .7722 Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.olean 241576 210872 .1270 Mathlib/Topology/Bornology/Hom.olean 341864 210872 .3831 Mathlib/Data/Polynomial/Inductions.olean 1125728 210736 .8128 Mathlib/MeasureTheory/Covering/Differentiation.olean 252568 210568 .1662 Mathlib/Data/Multiset/Functor.olean 371800 210328 .4342 Mathlib/Data/List/Card.olean 314216 209856 .3321 Mathlib/Algebra/Lie/Character.olean 522328 209528 .5988 Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.olean 394184 209488 .4685 Mathlib/Algebra/Order/Module.olean 260160 209400 .1951 Mathlib/Data/Fintype/CardEmbedding.olean 552224 208816 .6218 Mathlib/MeasureTheory/Integral/CircleTransform.olean 589944 208416 .6467 Mathlib/Dynamics/PeriodicPts.olean 273776 207776 .2410 Mathlib/Order/Max.olean 209368 207728 .0078 Mathlib/Algebra/Order/Monoid/Prod.olean 214856 207448 .0344 Mathlib/Algebra/GroupRingAction/Basic.olean 629528 207280 .6707 Mathlib/CategoryTheory/Closed/Functor.olean 302168 206800 .3156 Mathlib/Algebra/GroupWithZero/Units/Basic.olean 281440 206360 .2667 Mathlib/Data/Int/Interval.olean 645888 205984 .6810 Mathlib/Computability/Halting.olean 246512 205968 .1644 Mathlib/Algebra/Category/ModuleCat/Abelian.olean 285032 205784 .2780 Mathlib/Order/Filter/CountableInter.olean 799776 205336 .7432 Mathlib/Data/Polynomial/EraseLead.olean 205224 205224 .0000 Mathlib/Algebra/EuclideanDomain/Instances.olean 561576 205184 .6346 Mathlib/Analysis/BoxIntegral/Partition/Split.olean 458808 205016 .5531 Mathlib/Data/Nat/Interval.olean 479680 204904 .5728 Mathlib/Data/Set/Pairwise/Basic.olean 336512 204576 .3920 Mathlib/Algebra/Group/Conj.olean 288392 204536 .2907 Mathlib/LinearAlgebra/SModEq.olean 667336 204416 .6936 Mathlib/GroupTheory/Perm/Fin.olean 859416 204072 .7625 Mathlib/Analysis/SpecificLimits/Basic.olean 370640 204064 .4494 Mathlib/Topology/Algebra/Order/Floor.olean 256800 203864 .2061 Mathlib/Topology/Category/TopCat/Basic.olean 203832 203832 .0000 Mathlib/Tactic/LeftRight.olean 895376 203808 .7723 Mathlib/Analysis/Complex/CauchyIntegral.olean 338112 203496 .3981 Mathlib/Probability/ProbabilityMassFunction/Constructions.olean 339176 203232 .4008 Mathlib/Algebra/Module/Projective.olean 648848 202832 .6873 Mathlib/Analysis/Convex/Star.olean 212328 202352 .0469 Mathlib/Algebra/Order/EuclideanAbsoluteValue.olean 253144 202312 .2008 Mathlib/Tactic/Explode/Datatypes.olean 670720 202272 .6984 Mathlib/Analysis/LocallyConvex/Basic.olean 339256 202088 .4043 Mathlib/Topology/Algebra/Nonarchimedean/Basic.olean 653456 201736 .6912 Mathlib/Topology/MetricSpace/HausdorffDimension.olean 211168 201656 .0450 Mathlib/GroupTheory/GroupAction/Sum.olean 920032 201376 .7811 Mathlib/Analysis/SpecificLimits/Normed.olean 317472 201056 .3666 Mathlib/Order/Zorn.olean 251016 200808 .2000 Mathlib/Data/Finset/Slice.olean 487776 200416 .5891 Mathlib/FieldTheory/IsAlgClosed/Classification.olean 202768 200216 .0125 Mathlib/CategoryTheory/Functor/Functorial.olean 337888 200064 .4078 Mathlib/MeasureTheory/CardMeasurableSpace.olean 353064 199816 .4340 Mathlib/Topology/Sheaves/SheafCondition/Sites.olean 264064 199736 .2436 Mathlib/Control/Traversable/Equiv.olean 533824 199584 .6261 Mathlib/RingTheory/RingHom/Surjective.olean 523528 199520 .6188 Mathlib/Data/Real/Irrational.olean 199184 199184 .0000 Mathlib/Tactic/RSuffices.olean 577760 199152 .6553 Mathlib/SetTheory/Ordinal/FixedPoint.olean 209944 199056 .0518 Mathlib/Tactic/Continuity.olean 468664 198688 .5760 Mathlib/Data/Finset/Fold.olean 237192 198616 .1626 Mathlib/RingTheory/Valuation/Quotient.olean 902912 198576 .7800 Mathlib/Topology/ContinuousFunction/StoneWeierstrass.olean 342824 198496 .4209 Mathlib/Analysis/InnerProductSpace/LaxMilgram.olean 259360 198448 .2348 Mathlib/Logic/Unique.olean 789536 198256 .7488 Mathlib/Analysis/InnerProductSpace/Orientation.olean 1463272 197896 .8647 Mathlib/Analysis/Calculus/UniformLimitsDeriv.olean 452432 197872 .5626 Mathlib/Topology/List.olean 197704 197136 .0028 Mathlib/Algebra/Order/Positive/Field.olean 414856 196968 .5252 Mathlib/LinearAlgebra/AffineSpace/Midpoint.olean 216880 196840 .0924 Mathlib/Combinatorics/Quiver/SingleObj.olean 219032 196544 .1026 Mathlib/Algebra/Homology/ShortExact/Abelian.olean 227872 196144 .1392 Mathlib/Order/Filter/Interval.olean 211168 195664 .0734 Mathlib/CategoryTheory/Functor/InvIsos.olean 195288 195288 .0000 Mathlib/Tactic/ClearExcept.olean 1443784 194968 .8649 Mathlib/NumberTheory/Pell.olean 194744 194744 .0000 Mathlib/Algebra/Tropical/Lattice.olean 249520 194392 .2209 Mathlib/MeasureTheory/Measure/MutuallySingular.olean 196120 194264 .0094 Mathlib/CategoryTheory/Limits/Connected.olean 356592 194112 .4556 Mathlib/Data/Finsupp/Multiset.olean 638152 193952 .6960 Mathlib/Data/Nat/Totient.olean 515320 193904 .6237 Mathlib/AlgebraicTopology/DoldKan/Homotopies.olean 565136 193824 .6570 Mathlib/Data/List/Permutation.olean 216928 193096 .1098 Mathlib/CategoryTheory/Triangulated/Pretriangulated.olean 212288 193072 .0905 Mathlib/Algebra/ContinuedFractions/Computation/Basic.olean 234344 192648 .1779 Mathlib/MeasureTheory/Function/StronglyMeasurable/Lp.olean 497640 192544 .6130 Mathlib/Analysis/Calculus/FDerivAnalytic.olean 194296 192400 .0097 Mathlib/Data/QPF/Multivariate/Constructions/Comp.olean 370608 192208 .4813 Mathlib/MeasureTheory/Function/EssSup.olean 349616 191888 .4511 Mathlib/Order/Bounded.olean 576088 190968 .6685 Mathlib/RingTheory/PowerSeries/WellKnown.olean 286624 190456 .3355 Mathlib/CategoryTheory/IsConnected.olean 434648 190320 .5621 Mathlib/Topology/Algebra/Order/Field.olean 190216 190216 .0000 Mathlib/Lean/Expr/Traverse.olean 247024 190104 .2304 Mathlib/Data/Matrix/Hadamard.olean 361160 189792 .4744 Mathlib/Data/PNat/Factors.olean 272112 189512 .3035 Mathlib/Topology/Instances/NNReal.olean 192520 189080 .0178 Mathlib/Topology/UniformSpace/AbsoluteValue.olean 212528 188888 .1112 Mathlib/Data/Pi/Interval.olean 635968 188848 .7030 Mathlib/LinearAlgebra/Matrix/Block.olean 197712 188224 .0479 Mathlib/Topology/Sets/Order.olean 423216 187968 .5558 Mathlib/GroupTheory/DoubleCoset.olean 661472 187912 .7159 Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.olean 593488 187824 .6835 Mathlib/GroupTheory/Commutator.olean 876728 187424 .7862 Mathlib/LinearAlgebra/TensorProduct/Matrix.olean 644224 187408 .7090 Mathlib/Topology/MetricSpace/Infsep.olean 331984 186704 .4376 Mathlib/Topology/Instances/Real.olean 643904 186040 .7110 Mathlib/AlgebraicGeometry/RingedSpace.olean 1744432 185928 .8934 Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.olean 204352 185840 .0905 Mathlib/Algebra/Order/Group/OrderIso.olean 186904 185720 .0063 Mathlib/RingTheory/OreLocalization/OreSet.olean 249088 185464 .2554 Mathlib/Data/Finset/Interval.olean 769984 185424 .7591 Mathlib/MeasureTheory/Constructions/Prod/Integral.olean 196512 185232 .0574 Mathlib/GroupTheory/Subgroup/MulOpposite.olean 344376 184384 .4645 Mathlib/MeasureTheory/Measure/Haar/NormedSpace.olean 284680 184136 .3531 Mathlib/Algebra/Homology/ModuleCat.olean 1210952 184136 .8479 Mathlib/NumberTheory/Bernoulli.olean 218344 184088 .1568 Mathlib/Data/Multiset/Interval.olean 183992 183992 .0000 Mathlib/Tactic/Clear_.olean 464856 183768 .6046 Mathlib/RingTheory/Coprime/Basic.olean 641824 183672 .7138 Mathlib/Analysis/LocallyConvex/Bounded.olean 515560 183304 .6444 Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.olean 250368 183128 .2685 Mathlib/NumberTheory/Primorial.olean 208704 182768 .1242 Mathlib/Order/PFilter.olean 185968 182568 .0182 Mathlib/CategoryTheory/PEmpty.olean 313776 182544 .4182 Mathlib/CategoryTheory/Sites/InducedTopology.olean 319072 182064 .4293 Mathlib/Data/Nat/ForSqrt.olean 624144 181888 .7085 Mathlib/Analysis/PSeries.olean 544528 181728 .6662 Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.olean 328760 181696 .4473 Mathlib/Probability/ProbabilityMassFunction/Basic.olean 376272 181576 .5174 Mathlib/Topology/Algebra/Valuation.olean 413712 181520 .5612 Mathlib/MeasureTheory/Covering/DensityTheorem.olean 459936 181368 .6056 Mathlib/LinearAlgebra/DirectSum/Finsupp.olean 593624 181304 .6945 Mathlib/NumberTheory/Divisors.olean 520752 180784 .6528 Mathlib/AlgebraicTopology/DoldKan/Decomposition.olean 242552 180712 .2549 Mathlib/Order/PrimeIdeal.olean 614336 180480 .7062 Mathlib/GroupTheory/PGroup.olean 661376 180424 .7271 Mathlib/NumberTheory/Padics/PadicVal.olean 1044208 180128 .8274 Mathlib/Algebra/Lie/IdealOperations.olean 493320 180104 .6349 Mathlib/Geometry/Euclidean/Sphere/Basic.olean 849552 179560 .7886 Mathlib/Analysis/BoxIntegral/DivergenceTheorem.olean 818856 179472 .7808 Mathlib/GroupTheory/Perm/List.olean 179368 179368 .0000 Mathlib/CategoryTheory/ConcreteCategory/UnbundledHom.olean 416600 179160 .5699 Mathlib/Topology/UrysohnsLemma.olean 192280 179128 .0684 Mathlib/Data/Opposite.olean 178824 178824 .0000 Mathlib/Lean/System/IO.olean 180864 178824 .0112 Mathlib/Control/ULift.olean 294424 178152 .3949 Mathlib/Topology/Algebra/GroupWithZero.olean 177896 177896 .0000 Mathlib/AlgebraicTopology/DoldKan/Notations.olean 272312 177800 .3470 Mathlib/Order/Monotone/Monovary.olean 698152 177784 .7453 Mathlib/RingTheory/DiscreteValuationRing/Basic.olean 909136 177488 .8047 Mathlib/Combinatorics/Catalan.olean 469568 177256 .6225 Mathlib/Topology/Support.olean 479256 177232 .6301 Mathlib/Probability/Density.olean 295048 177200 .3994 Mathlib/CategoryTheory/Sites/CompatibleSheafification.olean 233648 176608 .2441 Mathlib/Topology/Algebra/MulAction.olean 286992 175776 .3875 Mathlib/Data/Nat/Count.olean 410416 175480 .5724 Mathlib/Data/Polynomial/Degree/TrailingDegree.olean 175472 175472 .0000 Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.olean 277856 175408 .3687 Mathlib/Analysis/SpecialFunctions/ExpDeriv.olean 723520 174400 .7589 Mathlib/Analysis/NormedSpace/Pointwise.olean 287992 173968 .3959 Mathlib/Order/Filter/Partial.olean 173784 173784 .0000 Mathlib/Algebra/Module/Prod.olean 184288 173560 .0582 Mathlib/CategoryTheory/EssentialImage.olean 186112 173200 .0693 Mathlib/Data/Real/ENatENNReal.olean 675280 173112 .7436 Mathlib/RingTheory/Localization/Module.olean 173008 173008 .0000 Mathlib/CategoryTheory/Abelian/Ext.olean 508032 173000 .6594 Mathlib/Analysis/SpecialFunctions/Pow/Continuity.olean 193456 172768 .1069 Mathlib/LinearAlgebra/FreeModule/Basic.olean 174632 171952 .0153 Mathlib/LinearAlgebra/GeneralLinearGroup.olean 187528 171848 .0836 Mathlib/Topology/Instances/RealVectorSpace.olean 524072 171632 .6725 Mathlib/Analysis/SpecialFunctions/Exp.olean 178056 171504 .0367 Mathlib/AlgebraicTopology/DoldKan/FunctorN.olean 382992 171496 .5522 Mathlib/Topology/DenseEmbedding.olean 293536 171440 .4159 Mathlib/Data/Multiset/FinsetOps.olean 356088 171224 .5191 Mathlib/Algebra/GroupPower/Ring.olean 292024 171008 .4144 Mathlib/Topology/StoneCech.olean 229752 170840 .2564 Mathlib/Deprecated/Ring.olean 192720 170784 .1138 Mathlib/Logic/Relator.olean 171672 170568 .0064 Mathlib/AlgebraicTopology/Nerve.olean 242248 170416 .2965 Mathlib/Topology/NhdsSet.olean 197464 170304 .1375 Mathlib/Topology/UniformSpace/CompareReals.olean 187432 169984 .0930 Mathlib/CategoryTheory/Sites/Coherent.olean 776704 169944 .7811 Mathlib/Data/Polynomial/Expand.olean 856456 169808 .8017 Mathlib/Analysis/MellinTransform.olean 329608 169256 .4864 Mathlib/Order/GameAdd.olean 702720 169144 .7593 Mathlib/Data/Polynomial/Monic.olean 383744 168760 .5602 Mathlib/Analysis/Normed/Group/HomCompletion.olean 682104 168704 .7526 Mathlib/MeasureTheory/Decomposition/SignedHahn.olean 168168 168168 .0000 Mathlib/Tactic/RestateAxiom.olean 440680 168168 .6183 Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.olean 212528 167776 .2105 Mathlib/GroupTheory/GroupAction/FixingSubgroup.olean 223856 167640 .2511 Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.olean 286216 167392 .4151 Mathlib/CategoryTheory/Subobject/FactorThru.olean 234792 167216 .2878 Mathlib/Order/Heyting/Boundary.olean 247520 166992 .3253 Mathlib/Data/Finset/Option.olean 167744 166784 .0057 Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.olean 522096 166672 .6807 Mathlib/Analysis/Normed/Group/Pointwise.olean 432128 166624 .6144 Mathlib/Data/Multiset/Powerset.olean 365208 165688 .5463 Mathlib/Data/List/BigOperators/Lemmas.olean 1139744 165248 .8550 Mathlib/Analysis/Calculus/FDerivSymmetric.olean 308296 164184 .4674 Mathlib/Topology/Algebra/Module/LinearPMap.olean 201264 164120 .1845 Mathlib/SetTheory/Cardinal/Continuum.olean 798592 163968 .7946 Mathlib/Analysis/NormedSpace/HahnBanach/Separation.olean 167432 163792 .0217 Mathlib/CategoryTheory/Category/GaloisConnection.olean 343816 163792 .5236 Mathlib/Algebra/Order/Group/Abs.olean 415280 163352 .6066 Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.olean 406056 162944 .5987 Mathlib/Analysis/Calculus/FDeriv/Comp.olean 351936 162824 .5373 Mathlib/MeasureTheory/Function/Egorov.olean 162656 162656 .0000 Mathlib/Util/MemoFix.olean 307424 162456 .4715 Mathlib/NumberTheory/VonMangoldt.olean 861976 162432 .8115 Mathlib/Data/Matrix/Rank.olean 300528 162216 .4602 Mathlib/ModelTheory/Types.olean 256128 162168 .3668 Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.olean 357448 161600 .5479 Mathlib/Topology/Sheaves/Sheafify.olean 167152 161368 .0346 Mathlib/Algebra/Order/Monoid/Defs.olean 162176 161240 .0057 Mathlib/Algebra/Module/Algebra.olean 1920376 160552 .9163 Mathlib/RingTheory/FinitePresentation.olean 165256 160440 .0291 Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.olean 376352 159944 .5750 Mathlib/RingTheory/Nilpotent.olean 159880 159880 .0000 Mathlib/Data/SProd.olean 215872 159784 .2598 Mathlib/Data/TwoPointing.olean 466400 159440 .6581 Mathlib/MeasureTheory/Measure/AEMeasurable.olean 328688 159304 .5153 Mathlib/Analysis/Calculus/Deriv/Add.olean 339360 158944 .5316 Mathlib/Data/Multiset/Pi.olean 187056 158888 .1505 Mathlib/CategoryTheory/Sites/Spaces.olean 343392 158760 .5376 Mathlib/Data/List/Rdrop.olean 784504 158520 .7979 Mathlib/MeasureTheory/Function/ContinuousMapDense.olean 588056 158392 .7306 Mathlib/Algebra/Polynomial/BigOperators.olean 158184 158184 .0000 Mathlib/Init/Data/Int/Bitwise.olean 251032 157872 .3711 Mathlib/GroupTheory/Subsemigroup/Center.olean 547952 157808 .7120 Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.olean 157776 157776 .0000 Mathlib/Util/WithWeakNamespace.olean 306480 157480 .4861 Mathlib/Data/Multiset/Fold.olean 222776 157312 .2938 Mathlib/Analysis/Calculus/Deriv/Polynomial.olean 452272 157312 .6521 Mathlib/Topology/UniformSpace/Equicontinuity.olean 578680 156416 .7297 Mathlib/RingTheory/Localization/Submodule.olean 242584 156400 .3552 Mathlib/Computability/EpsilonNFA.olean 287680 156264 .4568 Mathlib/Topology/Sober.olean 328280 156152 .5243 Mathlib/Topology/Algebra/Module/LocallyConvex.olean 551592 156120 .7169 Mathlib/Data/Int/Bitwise.olean 206584 156064 .2445 Mathlib/Data/Subtype.olean 699168 155264 .7779 Mathlib/CategoryTheory/Generator.olean 591960 155160 .7378 Mathlib/Analysis/Calculus/Series.olean 164504 154952 .0580 Mathlib/MeasureTheory/Function/StronglyMeasurable/Inner.olean 229008 154952 .3233 Mathlib/Combinatorics/Pigeonhole.olean 614712 154800 .7481 Mathlib/Data/Nat/Choose/Multinomial.olean 569576 154584 .7285 Mathlib/RingTheory/Adjoin/FG.olean 464896 154480 .6677 Mathlib/Analysis/Calculus/LocalExtr.olean 267128 154320 .4222 Mathlib/Data/Finsupp/NeLocus.olean 231672 153944 .3355 Mathlib/Probability/ProbabilityMassFunction/Uniform.olean 506144 153832 .6960 Mathlib/Analysis/Convex/Exposed.olean 431808 153680 .6441 Mathlib/Analysis/Complex/LocallyUniformLimit.olean 336568 153616 .5435 Mathlib/Data/Set/Sigma.olean 395800 153112 .6131 Mathlib/RingTheory/Polynomial/Eisenstein/Basic.olean 153680 152936 .0048 Mathlib/Algebra/Order/Group/Instances.olean 485632 152536 .6859 Mathlib/Analysis/Convex/Topology.olean 364488 152344 .5820 Mathlib/MeasureTheory/Group/Integration.olean 553760 152264 .7250 Mathlib/NumberTheory/Liouville/LiouvilleWith.olean 292544 151928 .4806 Mathlib/Analysis/Hofer.olean 668408 151784 .7729 Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.olean 977640 151728 .8448 Mathlib/NumberTheory/Multiplicity.olean 151488 151488 .0000 Mathlib/Data/Bracket.olean 333264 151232 .5462 Mathlib/Data/Fintype/BigOperators.olean 387640 151224 .6098 Mathlib/Data/Set/Intervals/Pi.olean 393224 150568 .6170 Mathlib/Data/Dfinsupp/WellFounded.olean 161896 150464 .0706 Mathlib/Topology/UniformSpace/Pi.olean 301096 150392 .5005 Mathlib/Data/Multiset/Nodup.olean 534648 150216 .7190 Mathlib/Analysis/Calculus/Deriv/Inv.olean 150104 150104 .0000 Mathlib/Algebra/Quotient.olean 246872 149832 .3930 Mathlib/GroupTheory/Subsemigroup/Centralizer.olean 584048 149640 .7437 Mathlib/MeasureTheory/Integral/MeanInequalities.olean 172104 149544 .1310 Mathlib/Topology/Algebra/Order/Group.olean 306576 149224 .5132 Mathlib/Topology/Algebra/InfiniteSum/Order.olean 304640 149032 .5107 Mathlib/Data/Nat/Factors.olean 582928 148608 .7450 Mathlib/MeasureTheory/Integral/PeakFunction.olean 173264 148456 .1431 Mathlib/CategoryTheory/Limits/Shapes/Reflexive.olean 245472 148360 .3956 Mathlib/Topology/Algebra/Constructions.olean 244104 148168 .3930 Mathlib/Logic/Function/Iterate.olean 147976 147976 .0000 Mathlib/Util/SynthesizeUsing.olean 148576 147920 .0044 Mathlib/Algebra/Category/ModuleCat/Algebra.olean 147464 147464 .0000 Mathlib/Tactic/UnsetOption.olean 512712 147440 .7124 Mathlib/Analysis/Analytic/IsolatedZeros.olean 350112 147120 .5797 Mathlib/AlgebraicTopology/DoldKan/PInfty.olean 179680 146648 .1838 Mathlib/Algebra/Lie/Semisimple.olean 146536 146536 .0000 Mathlib/Tactic/Trace.olean 169576 146056 .1386 Mathlib/Control/EquivFunctor.olean 742576 145976 .8034 Mathlib/Algebra/Lie/Engel.olean 145728 145728 .0000 Mathlib/Util/AssertNoSorry.olean 530808 145200 .7264 Mathlib/Analysis/Convex/Integral.olean 440320 144816 .6711 Mathlib/Data/Set/Pointwise/BigOperators.olean 265656 144688 .4553 Mathlib/Algebra/Order/Sub/Defs.olean 296680 144544 .5127 Mathlib/Topology/Algebra/Order/MonotoneContinuity.olean 261448 144432 .4475 Mathlib/Data/Num/Prime.olean 151336 144264 .0467 Mathlib/Data/Fintype/List.olean 226704 144184 .3639 Mathlib/MeasureTheory/Constructions/BorelSpace/ContinuousLinearMap.olean 156024 144144 .0761 Mathlib/GroupTheory/Perm/Subgroup.olean 177328 143576 .1903 Mathlib/CategoryTheory/Monoidal/Linear.olean 610336 143440 .7649 Mathlib/Algebra/Order/Rearrangement.olean 547272 143416 .7379 Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.olean 143896 143280 .0042 Mathlib/Data/Fin/SuccPred.olean 523560 143232 .7264 Mathlib/Analysis/MeanInequalitiesPow.olean 558648 142752 .7444 Mathlib/Analysis/Convex/Intrinsic.olean 431696 142648 .6695 Mathlib/SetTheory/Ordinal/Exponential.olean 161984 142624 .1195 Mathlib/CategoryTheory/Bicategory/Strict.olean 142240 142240 .0000 Mathlib/Tactic/GuardGoalNums.olean 200400 141880 .2920 Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.olean 206840 141512 .3158 Mathlib/LinearAlgebra/Matrix/Trace.olean 485648 141080 .7095 Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.olean 308304 141064 .5424 Mathlib/Analysis/Convex/Quasiconvex.olean 1135592 140944 .8758 Mathlib/Analysis/SpecialFunctions/Complex/Arg.olean 181480 140704 .2246 Mathlib/Data/PNat/Find.olean 158712 140688 .1135 Mathlib/MeasureTheory/Function/SpecialFunctions/Inner.olean 390472 140416 .6403 Mathlib/Algebra/ContinuedFractions/Computation/Translations.olean 252432 140304 .4441 Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.olean 139928 139928 .0000 Mathlib/Tactic/GuardHypNums.olean 139888 139888 .0000 Mathlib/CategoryTheory/Limits/Preserves/Filtered.olean 265712 139880 .4735 Mathlib/CategoryTheory/Simple.olean 247640 139816 .4354 Mathlib/Algebra/Hom/Iterate.olean 226184 139624 .3826 Mathlib/Analysis/Convex/Hull.olean 207384 139616 .3267 Mathlib/Analysis/Calculus/DiffContOnCl.olean 168480 139528 .1718 Mathlib/Analysis/Complex/Circle.olean 172584 139480 .1918 Mathlib/Algebra/Ring/CompTypeclasses.olean 140632 139464 .0083 Mathlib/Algebra/Ring/AddAut.olean 576600 139344 .7583 Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.olean 423712 139272 .6713 Mathlib/Data/Finset/Sigma.olean 240016 139264 .4197 Mathlib/Algebra/GroupWithZero/Units/Lemmas.olean 281440 139152 .5055 Mathlib/Data/MvPolynomial/Comap.olean 145504 139104 .0439 Mathlib/Algebra/Category/GroupCat/Images.olean 198272 139088 .2984 Mathlib/Topology/Bornology/Constructions.olean 359448 138984 .6133 Mathlib/NumberTheory/ADEInequality.olean 179840 138936 .2274 Mathlib/Algebra/Homology/ComplexShape.olean 224904 138352 .3848 Mathlib/Data/Nat/MaxPowDiv.olean 158088 138288 .1252 Mathlib/Topology/Sheaves/Sheaf.olean 466184 138272 .7033 Mathlib/NumberTheory/LegendreSymbol/ZModChar.olean 140224 138176 .0146 Mathlib/GroupTheory/GroupAction/Option.olean 209704 138112 .3413 Mathlib/Logic/Equiv/Fintype.olean 361384 137952 .6182 Mathlib/Data/Nat/Parity.olean 280968 137904 .5091 Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.olean 241576 137856 .4293 Mathlib/Order/Filter/Cofinite.olean 400208 137552 .6562 Mathlib/Topology/Sheaves/Functors.olean 422312 137144 .6752 Mathlib/LinearAlgebra/Matrix/Spectrum.olean 170496 136848 .1973 Mathlib/MeasureTheory/Lattice.olean 408752 136464 .6661 Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.olean 743480 136464 .8164 Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.olean 399888 136448 .6587 Mathlib/Combinatorics/Additive/Energy.olean 136248 136248 .0000 Mathlib/Util/Qq.olean 546968 136168 .7510 Mathlib/FieldTheory/Minpoly/Basic.olean 190632 136056 .2862 Mathlib/Algebra/Ring/Basic.olean 236832 135784 .4266 Mathlib/Order/PartialSups.olean 243000 135760 .4413 Mathlib/GroupTheory/Solvable.olean 146328 135696 .0726 Mathlib/Algebra/Order/Monoid/Units.olean 541680 135400 .7500 Mathlib/Data/Polynomial/Reverse.olean 212760 135368 .3637 Mathlib/Computability/NFA.olean 223368 135256 .3944 Mathlib/Dynamics/Ergodic/Ergodic.olean 465720 135240 .7096 Mathlib/NumberTheory/LegendreSymbol/Basic.olean 509656 135160 .7348 Mathlib/Probability/Martingale/Convergence.olean 652176 134864 .7932 Mathlib/NumberTheory/BernoulliPolynomials.olean 137280 134744 .0184 Mathlib/Algebra/Module/Opposites.olean 740408 134744 .8180 Mathlib/Analysis/SpecificLimits/FloorPow.olean 360376 134464 .6268 Mathlib/NumberTheory/Liouville/Measure.olean 379168 134432 .6454 Mathlib/Data/Nat/Log.olean 156880 134232 .1443 Mathlib/Combinatorics/Young/SemistandardTableau.olean 779656 133888 .8282 Mathlib/CategoryTheory/Adhesive.olean 262328 133712 .4902 Mathlib/Analysis/SpecialFunctions/Arsinh.olean 379288 133712 .6474 Mathlib/Algebra/GCDMonoid/Finset.olean 266176 133704 .4976 Mathlib/MeasureTheory/Measure/GiryMonad.olean 133376 133376 .0000 Mathlib/Init/Control/Combinators.olean 501640 133336 .7342 Mathlib/LinearAlgebra/Eigenspace/Minpoly.olean 725808 133328 .8163 Mathlib/Analysis/Calculus/Taylor.olean 134384 132808 .0117 Mathlib/Order/RelIso/Group.olean 135040 132736 .0170 Mathlib/Init/Data/Int/Basic.olean 402432 132384 .6710 Mathlib/MeasureTheory/Measure/Haar/Quotient.olean 325600 132336 .5935 Mathlib/Analysis/Complex/RemovableSingularity.olean 406696 132144 .6750 Mathlib/Analysis/NormedSpace/AddTorsorBases.olean 267416 132136 .5058 Mathlib/Dynamics/Ergodic/MeasurePreserving.olean 320104 131968 .5877 Mathlib/Analysis/Convex/Cone/Dual.olean 319872 131888 .5876 Mathlib/Analysis/LocallyConvex/Polar.olean 495528 131664 .7342 Mathlib/Analysis/SpecialFunctions/Log/Basic.olean 243416 131576 .4594 Mathlib/Topology/MetricSpace/ThickenedIndicator.olean 286256 131352 .5411 Mathlib/Order/Filter/Archimedean.olean 286432 131296 .5416 Mathlib/Algebra/Group/Semiconj.olean 141912 131008 .0768 Mathlib/Analysis/NormedSpace/Algebra.olean 148400 130984 .1173 Mathlib/Data/SetLike/Basic.olean 524464 130880 .7504 Mathlib/Analysis/Convex/Extreme.olean 565040 130824 .7684 Mathlib/Probability/Kernel/MeasurableIntegral.olean 286968 130776 .5442 Mathlib/Topology/LocallyFinite.olean 134512 130656 .0286 Mathlib/GroupTheory/GroupAction/Embedding.olean 343184 130584 .6194 Mathlib/LinearAlgebra/AffineSpace/Slope.olean 345936 130544 .6226 Mathlib/Data/List/Join.olean 237160 130504 .4497 Mathlib/Algebra/Regular/Basic.olean 138200 130224 .0577 Mathlib/Order/Hom/Set.olean 170800 130008 .2388 Mathlib/Data/Finsupp/Interval.olean 129776 129776 .0000 Mathlib/RingTheory/Flat.olean 222696 129144 .4200 Mathlib/Analysis/InnerProductSpace/EuclideanDist.olean 316016 129112 .5914 Mathlib/MeasureTheory/Measure/Doubling.olean 129688 129080 .0046 Mathlib/Algebra/Order/Group/WithTop.olean 144224 128784 .1070 Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.olean 433400 128480 .7035 Mathlib/Combinatorics/SetFamily/LYM.olean 342384 128032 .6260 Mathlib/Topology/MetricSpace/Contracting.olean 226432 127920 .4350 Mathlib/Data/Finsupp/AList.olean 232352 127856 .4497 Mathlib/LinearAlgebra/FreeModule/Finite/Rank.olean 225832 127768 .4342 Mathlib/RingTheory/MvPolynomial/Basic.olean 127744 127744 .0000 Mathlib/Data/Rat/Basic.olean 305664 127728 .5821 Mathlib/Data/Nat/GCD/Basic.olean 310736 127480 .5897 Mathlib/Data/Polynomial/Taylor.olean 565152 127480 .7744 Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.olean 666928 127296 .8091 Mathlib/GroupTheory/Exponent.olean 314744 127152 .5960 Mathlib/Order/OrderIsoNat.olean 522168 127080 .7566 Mathlib/Data/Polynomial/Degree/Lemmas.olean 188384 127072 .3254 Mathlib/Control/Fix.olean 127528 126888 .0050 Mathlib/CategoryTheory/Abelian/Subobject.olean 245104 126816 .4826 Mathlib/Data/Set/Intervals/OrdConnected.olean 191896 126800 .3392 Mathlib/Analysis/BoxIntegral/Partition/Measure.olean 155296 126792 .1835 Mathlib/Topology/Algebra/Ring/Ideal.olean 400736 126720 .6837 Mathlib/Analysis/SpecialFunctions/Log/Base.olean 246848 126560 .4872 Mathlib/Order/SuccPred/Limit.olean 1157432 126536 .8906 Mathlib/RingTheory/Polynomial/Bernstein.olean 451304 126440 .7198 Mathlib/Data/Polynomial/Lifts.olean 288872 126344 .5626 Mathlib/Topology/Filter.olean 572128 126256 .7793 Mathlib/Analysis/SpecialFunctions/Log/Deriv.olean 314192 126064 .5987 Mathlib/Analysis/LocallyConvex/AbsConvex.olean 239288 126024 .4733 Mathlib/Topology/Instances/EReal.olean 549264 125920 .7707 Mathlib/RingTheory/GradedAlgebra/Radical.olean 201128 125912 .3739 Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.olean 142456 125752 .1172 Mathlib/Data/Fintype/Units.olean 126968 125632 .0105 Mathlib/Algebra/Star/Prod.olean 478208 125504 .7375 Mathlib/Analysis/Convex/SpecificFunctions/Deriv.olean 804600 125376 .8441 Mathlib/Algebra/ContinuedFractions/Computation/Approximations.olean 1216992 125248 .8970 Mathlib/Geometry/Euclidean/Triangle.olean 125024 125024 .0000 Mathlib/Tactic/Eqns.olean 201696 124984 .3803 Mathlib/Algebra/IsPrimePow.olean 273496 124808 .5436 Mathlib/Data/MvPolynomial/Expand.olean 241048 124760 .4824 Mathlib/Data/Fin/Interval.olean 263392 124696 .5265 Mathlib/FieldTheory/Laurent.olean 177720 124512 .2993 Mathlib/Data/Fintype/Pi.olean 648184 124400 .8080 Mathlib/Data/Polynomial/HasseDeriv.olean 959048 124384 .8703 Mathlib/Topology/TietzeExtension.olean 124376 124376 .0000 Mathlib/Topology/Category/Profinite/Projective.olean 304032 124336 .5910 Mathlib/Combinatorics/SimpleGraph/StronglyRegular.olean 216136 124320 .4248 Mathlib/Algebra/Algebra/Subalgebra/Pointwise.olean 124224 124224 .0000 Mathlib/Control/EquivFunctor/Instances.olean 126280 124128 .0170 Mathlib/Data/Rat/Denumerable.olean 244056 124040 .4917 Mathlib/Data/Set/Countable.olean 683640 123992 .8186 Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.olean 140840 123952 .1199 Mathlib/Data/Int/LeastGreatest.olean 139560 123944 .1118 Mathlib/CategoryTheory/Abelian/Images.olean 608968 123904 .7965 Mathlib/Order/Height.olean 225248 123808 .4503 Mathlib/Data/Nat/Bits.olean 239400 123736 .4831 Mathlib/Data/List/Range.olean 220488 123680 .4390 Mathlib/Algebra/GCDMonoid/IntegrallyClosed.olean 139968 123672 .1164 Mathlib/Init/Core.olean 292336 123496 .5775 Mathlib/Data/Multiset/LocallyFinite.olean 318736 123488 .6125 Mathlib/Algebra/Order/Pointwise.olean 159112 123376 .2245 Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.olean 236576 123352 .4785 Mathlib/Probability/Process/Adapted.olean 281224 123168 .5620 Mathlib/RingTheory/Localization/Integer.olean 146808 123112 .1614 Mathlib/Init/Data/List/Lemmas.olean 138336 123104 .1101 Mathlib/Init/Control/Lawful.olean 208752 122968 .4109 Mathlib/Order/OrdContinuous.olean 132920 122944 .0750 Mathlib/Control/Bitraversable/Basic.olean 876784 122936 .8597 Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.olean 396976 122552 .6912 Mathlib/CategoryTheory/Sites/Canonical.olean 368272 122440 .6675 Mathlib/LinearAlgebra/Matrix/Diagonal.olean 159392 122400 .2320 Mathlib/CategoryTheory/LiftingProperties/Basic.olean 441264 122352 .7227 Mathlib/LinearAlgebra/Coevaluation.olean 1037648 122352 .8820 Mathlib/NumberTheory/SumFourSquares.olean 531024 121960 .7703 Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.olean 342424 121840 .6441 Mathlib/Analysis/Convex/Jensen.olean 162472 121704 .2509 Mathlib/Combinatorics/SimpleGraph/Partition.olean 567856 121608 .7858 Mathlib/RingTheory/Adjoin/Tower.olean 576344 121304 .7895 Mathlib/Analysis/NormedSpace/HahnBanach/Extension.olean 121144 121144 .0000 Mathlib/Util/SAFE.olean 133960 120960 .0970 Mathlib/Topology/Algebra/Order/UpperLower.olean 120704 120704 .0000 Mathlib/CategoryTheory/Limits/Unit.olean 120632 120632 .0000 Mathlib/Topology/Category/CompHaus/Projective.olean 371928 120464 .6761 Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.olean 318080 120336 .6216 Mathlib/ModelTheory/FinitelyGenerated.olean 359048 120264 .6650 Mathlib/Computability/DFA.olean 121416 120224 .0098 Mathlib/Data/Fintype/Sort.olean 440032 120216 .7268 Mathlib/Data/Nat/Multiplicity.olean 247896 120112 .5154 Mathlib/Data/MvPolynomial/CommRing.olean 329216 119944 .6356 Mathlib/Topology/NoetherianSpace.olean 123968 119824 .0334 Mathlib/CategoryTheory/Monoidal/Tor.olean 396968 119528 .6988 Mathlib/Data/Nat/Fib.olean 354296 119504 .6627 Mathlib/LinearAlgebra/TensorProductBasis.olean 147480 119432 .1901 Mathlib/Logic/Nonempty.olean 119424 119424 .0000 Mathlib/Tactic/Substs.olean 265368 119328 .5503 Mathlib/LinearAlgebra/Matrix/Dual.olean 175848 119320 .3214 Mathlib/Data/IsROrC/Lemmas.olean 211432 119192 .4362 Mathlib/Order/Extension/Linear.olean 446016 119056 .7330 Mathlib/Topology/Algebra/Polynomial.olean 119040 119040 .0000 Mathlib/Tactic/Use.olean 419096 118920 .7162 Mathlib/Analysis/NormedSpace/QuaternionExponential.olean 118720 118720 .0000 Mathlib/Algebra/Order/Group/TypeTags.olean 223240 118624 .4686 Mathlib/Order/Disjointed.olean 171736 118576 .3095 Mathlib/Algebra/Homology/ShortComplex/Homology.olean 723560 118360 .8364 Mathlib/Analysis/Calculus/ParametricIntegral.olean 368296 118304 .6787 Mathlib/LinearAlgebra/Basis/Bilinear.olean 1073992 118208 .8899 Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.olean 326024 118160 .6375 Mathlib/MeasureTheory/Measure/Portmanteau.olean 225552 118152 .4761 Mathlib/Algebra/MonoidAlgebra/Degree.olean 117696 117696 .0000 Mathlib/Init/Data/List/Instances.olean 811360 117672 .8549 Mathlib/Analysis/Convex/Join.olean 123560 117664 .0477 Mathlib/Logic/Equiv/Functor.olean 138048 117656 .1477 Mathlib/ModelTheory/Quotients.olean 306248 117592 .6160 Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.olean 324192 117432 .6377 Mathlib/Analysis/SpecialFunctions/JapaneseBracket.olean 117872 117040 .0070 Mathlib/CategoryTheory/IsomorphismClasses.olean 567872 117032 .7939 Mathlib/Analysis/Calculus/LagrangeMultipliers.olean 264312 116936 .5575 Mathlib/Analysis/Calculus/Dslope.olean 1164112 116920 .8995 Mathlib/NumberTheory/DiophantineApproximation.olean 116808 116808 .0000 Mathlib/Data/String/Defs.olean 360648 116456 .6770 Mathlib/Data/Int/Parity.olean 116392 116392 .0000 Mathlib/Data/QPF/Multivariate/Constructions/Quot.olean 134232 115952 .1361 Mathlib/RingTheory/Subsemiring/Pointwise.olean 241064 115952 .5189 Mathlib/Topology/MetricSpace/Antilipschitz.olean 411672 115736 .7188 Mathlib/Probability/Process/HittingTime.olean 235632 115720 .5088 Mathlib/Data/Nat/Lattice.olean 520640 115688 .7777 Mathlib/Data/Matrix/PEquiv.olean 136536 115608 .1532 Mathlib/RingTheory/Subring/Pointwise.olean 115264 115264 .0000 Mathlib/Tactic/Clear!.olean 283464 115256 .5934 Mathlib/Probability/Martingale/OptionalSampling.olean 194424 115240 .4072 Mathlib/Data/Set/Enumerate.olean 271616 115168 .5759 Mathlib/Algebra/Order/Field/Power.olean 370176 114944 .6894 Mathlib/Topology/Algebra/Order/LeftRightLim.olean 171584 114936 .3301 Mathlib/Analysis/Calculus/Deriv/Pow.olean 176576 114872 .3494 Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.olean 166808 114704 .3123 Mathlib/Algebra/Divisibility/Basic.olean 115304 114688 .0053 Mathlib/CategoryTheory/Monoidal/Types/Symmetric.olean 168088 114568 .3184 Mathlib/Algebra/Bounds.olean 212928 114536 .4620 Mathlib/Algebra/CharZero/Lemmas.olean 122376 114464 .0646 Mathlib/Init/Data/Quot.olean 212144 114192 .4617 Mathlib/Order/MinMax.olean 114152 114152 .0000 Mathlib/CategoryTheory/Closed/Zero.olean 113816 113816 .0000 Mathlib/Tactic/TypeCheck.olean 117272 113776 .0298 Mathlib/Algebra/CharP/Invertible.olean 312112 113560 .6361 Mathlib/RingTheory/Polynomial/ScaleRoots.olean 208960 113512 .4567 Mathlib/Data/Nat/Hyperoperation.olean 429800 113408 .7361 Mathlib/SetTheory/Ordinal/Principal.olean 113952 113376 .0050 Mathlib/Analysis/Normed/Group/BallSphere.olean 271208 113344 .5820 Mathlib/RingTheory/Localization/InvSubmonoid.olean 273608 113320 .5858 Mathlib/Data/MvPolynomial/Supported.olean 153736 113200 .2636 Mathlib/Logic/IsEmpty.olean 633512 112856 .8218 Mathlib/Algebra/BigOperators/Ring.olean 193808 112280 .4206 Mathlib/Topology/MetricSpace/ShrinkingLemma.olean 452912 112176 .7523 Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.olean 181488 112048 .3826 Mathlib/Data/Finset/Pi.olean 182872 111784 .3887 Mathlib/MeasureTheory/Measure/OpenPos.olean 427856 111664 .7390 Mathlib/Data/Option/NAry.olean 219920 111464 .4931 Mathlib/Data/Multiset/Sections.olean 175968 111408 .3668 Mathlib/Algebra/ContinuedFractions/Translations.olean 246360 111352 .5480 Mathlib/LinearAlgebra/Matrix/Circulant.olean 140368 111288 .2071 Mathlib/RingTheory/FreeRing.olean 131672 111136 .1559 Mathlib/Algebra/Category/ModuleCat/Projective.olean 390152 110864 .7158 Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.olean 873776 110792 .8732 Mathlib/Data/Polynomial/UnitTrinomial.olean 322728 110616 .6572 Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.olean 341632 110592 .6762 Mathlib/GroupTheory/Schreier.olean 726728 110376 .8481 Mathlib/Analysis/Normed/Group/AddCircle.olean 183296 110256 .3984 Mathlib/Data/Finset/PImage.olean 184136 110000 .4026 Mathlib/Algebra/Ring/Units.olean 870712 109912 .8737 Mathlib/Analysis/BoxIntegral/Integrability.olean 253808 109760 .5675 Mathlib/Data/Set/Intervals/Disjoint.olean 241672 109520 .5468 Mathlib/RingTheory/MvPolynomial/Tower.olean 207496 109368 .4729 Mathlib/Data/Bitvec/Basic.olean 152656 109256 .2842 Mathlib/LinearAlgebra/AffineSpace/Pointwise.olean 436984 109160 .7501 Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.olean 375912 109144 .7096 Mathlib/Data/QPF/Multivariate/Basic.olean 109064 109064 .0000 Mathlib/CategoryTheory/Localization/Opposite.olean 183256 108896 .4057 Mathlib/Analysis/SpecialFunctions/Sqrt.olean 328344 108752 .6687 Mathlib/Algebra/GCDMonoid/Multiset.olean 373984 108680 .7093 Mathlib/RingTheory/Polynomial/Pochhammer.olean 340312 108568 .6809 Mathlib/Data/Matrix/Basis.olean 267592 107920 .5966 Mathlib/Topology/MetricSpace/PartitionOfUnity.olean 110792 107912 .0259 Mathlib/GroupTheory/Submonoid/Center.olean 108592 107880 .0065 Mathlib/Data/Int/Cast/Prod.olean 218224 107840 .5058 Mathlib/Topology/MetricSpace/Holder.olean 214752 107800 .4980 Mathlib/RingTheory/IntegrallyClosed.olean 143152 107648 .2480 Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.olean 152792 107528 .2962 Mathlib/Dynamics/Minimal.olean 107456 107456 .0000 Mathlib/Util/IncludeStr.olean 229464 107352 .5321 Mathlib/CategoryTheory/ConcreteCategory/Elementwise.olean 366264 107328 .7069 Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.olean 119112 107024 .1014 Mathlib/Algebra/Star/Pi.olean 146336 106792 .2702 Mathlib/Analysis/Calculus/FDeriv/Star.olean 247344 106632 .5688 Mathlib/LinearAlgebra/Charpoly/Basic.olean 106600 106600 .0000 Mathlib/Data/Rat/Star.olean 106496 106496 .0000 Mathlib/Algebra/GroupRingAction/Subobjects.olean 131712 106368 .1924 Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.olean 196096 106216 .4583 Mathlib/Data/Finset/Preimage.olean 212168 106104 .4999 Mathlib/LinearAlgebra/AnnihilatingPolynomial.olean 106080 106080 .0000 Mathlib/Data/ZMod/Algebra.olean 857160 106080 .8762 Mathlib/Analysis/SpecialFunctions/Stirling.olean 374696 106008 .7170 Mathlib/Analysis/LocallyConvex/BalancedCoreHull.olean 338160 105776 .6872 Mathlib/Topology/MetricSpace/Metrizable.olean 935240 105736 .8869 Mathlib/Algebra/Group/Ext.olean 105720 105720 .0000 Mathlib/Util/Pickle.olean 420600 105552 .7490 Mathlib/NumberTheory/Padics/PadicNorm.olean 408152 105480 .7415 Mathlib/Data/Polynomial/DenomsClearable.olean 144408 105368 .2703 Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.olean 206736 105008 .4920 Mathlib/Algebra/FreeMonoid/Count.olean 172032 104856 .3904 Mathlib/Data/PNat/Prime.olean 104560 104560 .0000 Mathlib/Lean/Json.olean 116640 104504 .1040 Mathlib/Data/Multiset/Sort.olean 104408 104408 .0000 Mathlib/LinearAlgebra/AffineSpace/Basic.olean 175336 104152 .4059 Mathlib/Data/List/Destutter.olean 456800 104096 .7721 Mathlib/RingTheory/Polynomial/Vieta.olean 171304 104088 .3923 Mathlib/Order/WellFounded.olean 257672 103944 .5966 Mathlib/Data/List/Intervals.olean 176456 103888 .4112 Mathlib/RingTheory/Polynomial/Tower.olean 266296 103888 .6098 Mathlib/Analysis/Complex/RealDeriv.olean 103752 103752 .0000 Mathlib/Algebra/Ring/OrderSynonym.olean 113840 103696 .0891 Mathlib/Topology/Order/Lattice.olean 435864 103664 .7621 Mathlib/Analysis/SpecialFunctions/Pow/Complex.olean 817672 103504 .8734 Mathlib/RingTheory/Polynomial/GaussLemma.olean 164392 103496 .3704 Mathlib/Data/Multiset/Dedup.olean 112672 103376 .0825 Mathlib/RingTheory/Localization/Away/AdjoinRoot.olean 358568 103376 .7116 Mathlib/Probability/Kernel/WithDensity.olean 272496 103344 .6207 Mathlib/Data/Set/Intervals/Group.olean 196384 103296 .4740 Mathlib/Data/Finset/NatAntidiagonal.olean 427960 103088 .7591 Mathlib/Analysis/Convex/Caratheodory.olean 156664 102936 .3429 Mathlib/Topology/Algebra/UniformFilterBasis.olean 148776 102840 .3087 Mathlib/Logic/Nontrivial.olean 225192 102696 .5439 Mathlib/Data/List/ToFinsupp.olean 135760 102304 .2464 Mathlib/RingTheory/DedekindDomain/Basic.olean 254032 102304 .5972 Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.olean 156880 102152 .3488 Mathlib/Data/Nat/PSub.olean 223672 102104 .5435 Mathlib/Combinatorics/Quiver/Push.olean 122792 102016 .1691 Mathlib/Order/KrullDimension.olean 190552 101912 .4651 Mathlib/GroupTheory/Perm/Option.olean 362088 101536 .7195 Mathlib/Analysis/SpecialFunctions/Polynomials.olean 167872 101096 .3977 Mathlib/Analysis/Normed/MulAction.olean 251240 100928 .5982 Mathlib/FieldTheory/Tower.olean 102024 100440 .0155 Mathlib/GroupTheory/Subgroup/Actions.olean 446824 100264 .7756 Mathlib/Analysis/NormedSpace/ConformalLinearMap.olean 196912 100048 .4919 Mathlib/LinearAlgebra/Matrix/Charpoly/Minpoly.olean 189752 99992 .4730 Mathlib/RingTheory/Polynomial/Opposites.olean 138864 99920 .2804 Mathlib/Algebra/Category/ModuleCat/EpiMono.olean 99888 99888 .0000 Mathlib/Tactic/ApplyWith.olean 357136 99744 .7207 Mathlib/Geometry/Euclidean/Sphere/SecondInter.olean 659016 99696 .8487 Mathlib/Analysis/Calculus/Monotone.olean 209136 99568 .5239 Mathlib/SetTheory/Ordinal/CantorNormalForm.olean 221016 99400 .5502 Mathlib/Data/MvPolynomial/PDeriv.olean 98928 98928 .0000 Mathlib/Data/Rat/Init.olean 98896 98896 .0000 Mathlib/Util/AssertExists.olean 215656 98792 .5419 Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.olean 152904 98464 .3560 Mathlib/Data/Set/Intervals/OrderIso.olean 120032 98032 .1832 Mathlib/Data/Int/Range.olean 245600 97960 .6011 Mathlib/Data/Finset/MulAntidiagonal.olean 249248 97808 .6075 Mathlib/RingTheory/DedekindDomain/Factorization.olean 155792 97744 .3725 Mathlib/Data/Int/ConditionallyCompleteOrder.olean 98280 97656 .0063 Mathlib/CategoryTheory/Functor/Hom.olean 191384 97224 .4919 Mathlib/Combinatorics/Quiver/Subquiver.olean 211224 96984 .5408 Mathlib/Data/Nat/Size.olean 200736 96928 .5171 Mathlib/Topology/Algebra/InfiniteSum/Module.olean 179440 96880 .4600 Mathlib/Data/Set/Intervals/ProjIcc.olean 215104 96840 .5497 Mathlib/Analysis/Analytic/RadiusLiminf.olean 120720 96784 .1982 Mathlib/Logic/Small/Basic.olean 289432 96768 .6656 Mathlib/Topology/MetricSpace/Completion.olean 142072 96688 .3194 Mathlib/CategoryTheory/Limits/MonoCoprod.olean 423760 96448 .7723 Mathlib/RingTheory/Ideal/MinimalPrime.olean 96440 96440 .0000 Mathlib/Data/QPF/Multivariate/Constructions/Prj.olean 188208 96264 .4885 Mathlib/Analysis/Calculus/ParametricIntervalIntegral.olean 266544 96144 .6392 Mathlib/Deprecated/Subfield.olean 96000 96000 .0000 Mathlib/Data/HashMap.olean 102040 95832 .0608 Mathlib/CategoryTheory/Limits/FullSubcategory.olean 155904 95808 .3854 Mathlib/Data/List/Prime.olean 346960 95800 .7238 Mathlib/Topology/MetricSpace/Kuratowski.olean 344104 95728 .7218 Mathlib/Analysis/Convex/Uniform.olean 533392 95712 .8205 Mathlib/Topology/Perfect.olean 622152 95624 .8463 Mathlib/Data/Real/Pi/Wallis.olean 113032 95520 .1549 Mathlib/Data/FunLike/Equiv.olean 285016 95496 .6649 Mathlib/Analysis/Calculus/Deriv/ZPow.olean 95336 95336 .0000 Mathlib/Tactic/Constructor.olean 423600 95264 .7751 Mathlib/Analysis/SpecialFunctions/Complex/Log.olean 328264 94784 .7112 Mathlib/Topology/LocalAtTarget.olean 159320 94712 .4055 Mathlib/Order/Minimal.olean 229176 94640 .5870 Mathlib/Data/Fintype/Sum.olean 718040 94616 .8682 Mathlib/RingTheory/DedekindDomain/PID.olean 127008 94408 .2566 Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.olean 134496 94360 .2984 Mathlib/Data/Fin/Tuple/Monotone.olean 94248 94248 .0000 Mathlib/Init/Data/Nat/Notation.olean 1203336 94248 .9216 Mathlib/Analysis/Convex/SpecificFunctions/Basic.olean 292104 94048 .6780 Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.olean 209656 93936 .5519 Mathlib/LinearAlgebra/Matrix/IsDiag.olean 137528 93928 .3170 Mathlib/Order/PropInstances.olean 277832 93864 .6621 Mathlib/Dynamics/Ergodic/Conservative.olean 93672 93672 .0000 Mathlib/Topology/Sheaves/Abelian.olean 155240 93528 .3975 Mathlib/Topology/Instances/Irrational.olean 248488 93496 .6237 Mathlib/Data/Set/Pairwise/Lattice.olean 151760 93448 .3842 Mathlib/Combinatorics/DoubleCounting.olean 93216 93216 .0000 Mathlib/Lean/CoreM.olean 92880 92880 .0000 Mathlib/Geometry/Manifold/ConformalGroupoid.olean 205896 92792 .5493 Mathlib/Topology/Algebra/InfiniteSum/Ring.olean 528608 92720 .8245 Mathlib/Algebra/QuadraticDiscriminant.olean 260448 92568 .6445 Mathlib/Combinatorics/Derangements/Finite.olean 100744 92416 .0826 Mathlib/GroupTheory/Submonoid/Centralizer.olean 387864 92400 .7617 Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.olean 888784 92384 .8960 Mathlib/FieldTheory/PrimitiveElement.olean 292384 92096 .6850 Mathlib/RingTheory/Polynomial/RationalRoot.olean 164752 92024 .4414 Mathlib/Algebra/Lie/CartanSubalgebra.olean 791440 91944 .8838 Mathlib/Analysis/Convex/StoneSeparation.olean 425712 91920 .7840 Mathlib/Data/Rat/Lemmas.olean 308736 91904 .7023 Mathlib/Analysis/ODE/Gronwall.olean 91864 91864 .0000 Mathlib/Data/Array/Defs.olean 91840 91840 .0000 Mathlib/Lean/Expr/ReplaceRec.olean 225880 91744 .5938 Mathlib/Topology/MetricSpace/CauSeqFilter.olean 93280 91704 .0168 Mathlib/Order/UpperLower/Hom.olean 355608 91424 .7429 Mathlib/Combinatorics/SimpleGraph/Trails.olean 91416 91416 .0000 Mathlib/Util/Tactic.olean 245768 91376 .6282 Mathlib/Data/Nat/Pairing.olean 352944 91368 .7411 Mathlib/Analysis/Calculus/LHopital.olean 480016 90984 .8104 Mathlib/Probability/Integration.olean 210528 90888 .5682 Mathlib/Data/Set/Intervals/Monotone.olean 112560 90736 .1938 Mathlib/Data/Int/SuccPred.olean 101888 90624 .1105 Mathlib/Order/Atoms/Finite.olean 141272 90616 .3585 Mathlib/Control/Bitraversable/Lemmas.olean 90296 90296 .0000 Mathlib/Data/Fintype/Vector.olean 111656 90224 .1919 Mathlib/Order/CompleteLatticeIntervals.olean 277248 90224 .6745 Mathlib/Analysis/Complex/Schwarz.olean 90176 90176 .0000 Mathlib/Tactic/Existsi.olean 90064 90064 .0000 Mathlib/Data/ListM/Heartbeats.olean 193680 89984 .5353 Mathlib/Data/List/Dedup.olean 142688 89960 .3695 Mathlib/Analysis/Calculus/FDeriv/Linear.olean 104160 89888 .1370 Mathlib/Data/Char.olean 98272 89848 .0857 Mathlib/Order/RelIso/Set.olean 199544 89752 .5502 Mathlib/RingTheory/Bezout.olean 342600 89640 .7383 Mathlib/LinearAlgebra/AffineSpace/Matrix.olean 210456 89600 .5742 Mathlib/SetTheory/Cardinal/SchroederBernstein.olean 263904 89352 .6614 Mathlib/Algebra/GroupWithZero/Power.olean 100944 89280 .1155 Mathlib/CategoryTheory/Noetherian.olean 261552 89280 .6586 Mathlib/Data/Set/UnionLift.olean 97600 89176 .0863 Mathlib/Topology/Algebra/Star.olean 117624 89152 .2420 Mathlib/Algebra/Order/Sub/WithTop.olean 576176 89152 .8452 Mathlib/Combinatorics/Additive/PluenneckeRuzsa.olean 232528 88880 .6177 Mathlib/Analysis/Calculus/Deriv/Slope.olean 88808 88808 .0000 Mathlib/Init/Data/Ordering/Basic.olean 88696 88696 .0000 Mathlib/Tactic/RelCongr/Basic.olean 89528 88696 .0092 Mathlib/CategoryTheory/Functor/ReflectsIso.olean 212872 88584 .5838 Mathlib/Analysis/Convex/Normed.olean 242080 88560 .6341 Mathlib/NumberTheory/Liouville/LiouvilleNumber.olean 255048 88464 .6531 Mathlib/Algebra/MonoidAlgebra/Support.olean 157488 88104 .4405 Mathlib/Order/SemiconjSup.olean 198928 88008 .5575 Mathlib/Algebra/Order/Ring/Abs.olean 146928 87848 .4021 Mathlib/Data/List/ProdSigma.olean 600696 87712 .8539 Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.olean 104016 87680 .1570 Mathlib/CategoryTheory/ConcreteCategory/Bundled.olean 87488 87488 .0000 Mathlib/Data/Rat/Encodable.olean 96240 87320 .0926 Mathlib/Order/Synonym.olean 151888 87048 .4268 Mathlib/Analysis/Calculus/Conformal/NormedSpace.olean 464760 87024 .8127 Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.olean 210040 86896 .5862 Mathlib/Data/Nat/Pow.olean 86704 86704 .0000 Mathlib/Algebra/Group/WithOne/Units.olean 307352 86384 .7189 Mathlib/RingTheory/Localization/NumDen.olean 196160 86328 .5599 Mathlib/Algebra/BigOperators/Pi.olean 252464 86240 .6584 Mathlib/SetTheory/Cardinal/Divisibility.olean 256256 86168 .6637 Mathlib/Data/Bool/Count.olean 600656 86040 .8567 Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.olean 242920 85728 .6470 Mathlib/Analysis/Convex/SpecificFunctions/Pow.olean 151192 85584 .4339 Mathlib/Algebra/ContinuedFractions/TerminatedStable.olean 186320 85024 .5436 Mathlib/Topology/Covering.olean 337448 84960 .7482 Mathlib/Data/Set/Intervals/OrdConnectedComponent.olean 394152 84760 .7849 Mathlib/MeasureTheory/Integral/Layercake.olean 176680 84680 .5207 Mathlib/Data/Multiset/Lattice.olean 100504 84544 .1588 Mathlib/Data/Nat/SuccPred.olean 90400 84504 .0652 Mathlib/Init/Data/Sigma/Basic.olean 1351176 84344 .9375 Mathlib/AlgebraicTopology/DoldKan/Faces.olean 84328 84328 .0000 Mathlib/CategoryTheory/Monoidal/Skeleton.olean 304896 84208 .7238 Mathlib/Combinatorics/SimpleGraph/IncMatrix.olean 150472 84088 .4411 Mathlib/Algebra/Order/Monoid/MinMax.olean 177232 83928 .5264 Mathlib/MeasureTheory/Measure/AEDisjoint.olean 320616 83816 .7385 Mathlib/Probability/Martingale/OptionalStopping.olean 100632 83720 .1680 Mathlib/Data/Nat/Cast/Prod.olean 186352 83592 .5514 Mathlib/GroupTheory/Subsemigroup/Membership.olean 268888 83520 .6893 Mathlib/Topology/GDelta.olean 83504 83504 .0000 Mathlib/CategoryTheory/Limits/SmallComplete.olean 96176 83392 .1329 Mathlib/Topology/Order/Priestley.olean 143752 83360 .4201 Mathlib/Algebra/Ring/Idempotents.olean 1025448 83200 .9188 Mathlib/Analysis/Convex/Slope.olean 391376 82888 .7882 Mathlib/Probability/Martingale/Centering.olean 117224 82856 .2931 Mathlib/Analysis/Calculus/Deriv/AffineMap.olean 85856 82848 .0350 Mathlib/Data/Finite/Basic.olean 364320 82824 .7726 Mathlib/Data/Polynomial/Mirror.olean 373864 82784 .7785 Mathlib/LinearAlgebra/Vandermonde.olean 350720 82640 .7643 Mathlib/SetTheory/Ordinal/Topology.olean 147672 82608 .4405 Mathlib/Order/Filter/SmallSets.olean 129000 82560 .3600 Mathlib/Data/Finset/Pairwise.olean 419688 82560 .8032 Mathlib/RingTheory/Polynomial/Selmer.olean 90392 82416 .0882 Mathlib/Data/ULift.olean 194792 82304 .5774 Mathlib/Analysis/Normed/Group/InfiniteSum.olean 131672 82144 .3761 Mathlib/LinearAlgebra/Matrix/Symmetric.olean 99592 82056 .1760 Mathlib/Data/FunLike/Basic.olean 165104 81880 .5040 Mathlib/Order/Filter/EventuallyConst.olean 114072 81816 .2827 Mathlib/Combinatorics/SimpleGraph/Hasse.olean 240440 81680 .6602 Mathlib/Data/Finsupp/BigOperators.olean 141000 81672 .4207 Mathlib/Analysis/SpecialFunctions/Complex/Circle.olean 309536 81600 .7363 Mathlib/Geometry/Euclidean/Inversion.olean 349832 81512 .7669 Mathlib/CategoryTheory/Idempotents/Basic.olean 317960 81392 .7440 Mathlib/Analysis/Asymptotics/SpecificAsymptotics.olean 441744 81088 .8164 Mathlib/Data/Real/Pi/Leibniz.olean 82016 80960 .0128 Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.olean 311216 80928 .7399 Mathlib/Data/Polynomial/IntegralNormalization.olean 81000 80432 .0070 Mathlib/Algebra/Ring/Fin.olean 318472 80160 .7482 Mathlib/Data/Real/Cardinality.olean 106648 80088 .2490 Mathlib/Data/Fintype/Prod.olean 702984 79784 .8865 Mathlib/NumberTheory/FermatPsp.olean 136384 79688 .4157 Mathlib/Data/Set/List.olean 148800 79656 .4646 Mathlib/Control/Traversable/Lemmas.olean 168448 79624 .5273 Mathlib/Algebra/Regular/SMul.olean 80696 79376 .0163 Mathlib/Data/QPF/Multivariate/Constructions/Const.olean 126176 79248 .3719 Mathlib/Algebra/CharP/Algebra.olean 115328 79240 .3129 Mathlib/Dynamics/FixedPoints/Basic.olean 219832 79200 .6397 Mathlib/Analysis/Convex/Independent.olean 229616 78984 .6560 Mathlib/NumberTheory/LSeries.olean 83592 78736 .0580 Mathlib/Data/Countable/Basic.olean 167200 78704 .5292 Mathlib/Topology/UrysohnsBounded.olean 98416 78400 .2033 Mathlib/Algebra/Ring/Regular.olean 82040 78392 .0444 Mathlib/Tactic/RelCongr.olean 87880 78344 .1085 Mathlib/Data/Countable/Defs.olean 82016 78328 .0449 Mathlib/Tactic/GCongr.olean 221984 78320 .6471 Mathlib/Analysis/NormedSpace/IsROrC.olean 78232 78232 .0000 Mathlib/Algebra/Group/ConjFinite.olean 127288 78152 .3860 Mathlib/Topology/Instances/Int.olean 78784 77992 .0100 Mathlib/CategoryTheory/Category/KleisliCat.olean 154984 77744 .4983 Mathlib/Order/SuccPred/IntervalSucc.olean 192352 77600 .5965 Mathlib/Data/Set/MulAntidiagonal.olean 168392 77448 .5400 Mathlib/Order/Iterate.olean 78528 77432 .0139 Mathlib/Init/Data/List/Basic.olean 77040 77040 .0000 Mathlib/Algebra/CharP/Subring.olean 141008 76896 .4546 Mathlib/Data/Multiset/Sum.olean 744712 76896 .8967 Mathlib/AlgebraicTopology/DoldKan/Degeneracies.olean 76768 76768 .0000 Mathlib/Topology/Algebra/Localization.olean 120000 76624 .3614 Mathlib/ModelTheory/Graph.olean 77080 76496 .0075 Mathlib/Algebra/Order/Nonneg/Floor.olean 118256 76488 .3532 Mathlib/SetTheory/Cardinal/Finite.olean 76616 76192 .0055 Mathlib/Algebra/Order/Group/Units.olean 85936 76168 .1136 Mathlib/Data/MvPolynomial/Counit.olean 190592 76096 .6007 Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.olean 521672 76048 .8542 Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.olean 275848 75952 .7246 Mathlib/Algebra/Squarefree.olean 76648 75928 .0093 Mathlib/Topology/Category/Locale.olean 385704 75904 .8032 Mathlib/RingTheory/Coprime/Lemmas.olean 125152 75816 .3942 Mathlib/Data/List/Sections.olean 143168 75728 .4710 Mathlib/Data/Set/Constructions.olean 420032 75640 .8199 Mathlib/RingTheory/RootsOfUnity/Minpoly.olean 382752 75616 .8024 Mathlib/Analysis/Complex/Conformal.olean 171440 75600 .5590 Mathlib/Data/Int/Cast/Basic.olean 85848 75368 .1220 Mathlib/Data/Set/Functor.olean 144344 75152 .4793 Mathlib/Analysis/Calculus/Deriv/Inverse.olean 94696 74800 .2101 Mathlib/Init/Data/Int/Order.olean 254784 74400 .7079 Mathlib/ModelTheory/Skolem.olean 148088 74352 .4979 Mathlib/Combinatorics/Quiver/Cast.olean 128184 74280 .4205 Mathlib/Data/Vector/Mem.olean 194336 74248 .6179 Mathlib/Data/Set/Intervals/WithBotTop.olean 236240 74216 .6858 Mathlib/Combinatorics/SetFamily/Intersecting.olean 74144 74144 .0000 Mathlib/Util/Time.olean 146624 73904 .4959 Mathlib/Algebra/GroupWithZero/Divisibility.olean 162008 73880 .5439 Mathlib/Data/Nat/Sqrt.olean 81048 73872 .0885 Mathlib/CategoryTheory/Subobject/WellPowered.olean 168360 73488 .5635 Mathlib/Probability/Independence/ZeroOne.olean 126952 73040 .4246 Mathlib/Algebra/Ring/Commute.olean 79488 72368 .0895 Mathlib/Algebra/FreeNonUnitalNonAssocAlgebra.olean 221920 72344 .6740 Mathlib/Algebra/CharZero/Quotient.olean 145912 72296 .5045 Mathlib/Topology/MetricSpace/MetricSeparated.olean 453624 71904 .8414 Mathlib/Data/Nat/Choose/Sum.olean 349744 71896 .7944 Mathlib/RingTheory/Ideal/AssociatedPrime.olean 228936 71680 .6868 Mathlib/Data/Multiset/Antidiagonal.olean 371816 71664 .8072 Mathlib/RingTheory/RingHomProperties.olean 235544 71624 .6959 Mathlib/FieldTheory/SeparableDegree.olean 413608 71608 .8268 Mathlib/Analysis/Calculus/ExtendDeriv.olean 90688 71424 .2124 Mathlib/GroupTheory/Subgroup/Simple.olean 78112 71176 .0887 Mathlib/Data/Set/Opposite.olean 131904 71160 .4605 Mathlib/Data/List/TFAE.olean 74912 70928 .0531 Mathlib/Algebra/Hom/Embedding.olean 374392 70848 .8107 Mathlib/Combinatorics/Hall/Finite.olean 143048 70840 .5047 Mathlib/Analysis/LocallyConvex/StrongTopology.olean 250792 70800 .7176 Mathlib/Analysis/SpecialFunctions/CompareExp.olean 135400 70784 .4772 Mathlib/Algebra/Ring/Divisibility.olean 132560 70696 .4666 Mathlib/Topology/Algebra/Affine.olean 166552 70376 .5774 Mathlib/Data/List/NatAntidiagonal.olean 206272 70240 .6594 Mathlib/LinearAlgebra/ProjectiveSpace/Independence.olean 70752 70136 .0087 Mathlib/Algebra/Order/Group/Prod.olean 442656 69928 .8420 Mathlib/MeasureTheory/Covering/LiminfLimsup.olean 145464 69680 .5209 Mathlib/MeasureTheory/Function/AEMeasurableSequence.olean 292664 69496 .7625 Mathlib/Probability/CondCount.olean 164304 69264 .5784 Mathlib/Data/Real/ConjugateExponents.olean 145064 68976 .5245 Mathlib/LinearAlgebra/Matrix/DotProduct.olean 859464 68928 .9198 Mathlib/Topology/Category/Profinite/CofilteredLimit.olean 159984 68624 .5710 Mathlib/Algebra/Order/Chebyshev.olean 250080 68472 .7262 Mathlib/MeasureTheory/Group/GeometryOfNumbers.olean 172464 68272 .6041 Mathlib/Data/Finsupp/Antidiagonal.olean 130224 68168 .4765 Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.olean 108424 68048 .3723 Mathlib/Logic/Function/Conjugate.olean 116720 67896 .4183 Mathlib/Data/Finset/Sum.olean 182448 67880 .6279 Mathlib/Analysis/Convex/Extrema.olean 95888 67768 .2932 Mathlib/Data/Finsupp/Indicator.olean 105096 67744 .3554 Mathlib/Analysis/Calculus/Deriv/Prod.olean 67584 67584 .0000 Mathlib/LinearAlgebra/Matrix/FiniteDimensional.olean 148144 67584 .5437 Mathlib/Data/Finite/Card.olean 67456 67456 .0000 Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.olean 71000 67456 .0499 Mathlib/Logic/Equiv/Nat.olean 129864 67304 .4817 Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.olean 268600 67208 .7497 Mathlib/Topology/MetricSpace/CantorScheme.olean 119208 66992 .4380 Mathlib/Topology/Instances/Rat.olean 108504 66928 .3831 Mathlib/Algebra/CharZero/Defs.olean 104152 66728 .3593 Mathlib/Analysis/Calculus/Conformal/InnerProduct.olean 301216 66552 .7790 Mathlib/Topology/Category/TopCat/Limits/Konig.olean 66456 66456 .0000 Mathlib/Topology/Category/Born.olean 421200 66416 .8423 Mathlib/RingTheory/EisensteinCriterion.olean 142944 66320 .5360 Mathlib/Algebra/CharP/Two.olean 118408 66288 .4401 Mathlib/Topology/Instances/Nat.olean 136472 66088 .5157 Mathlib/Algebra/Order/Group/MinMax.olean 82744 66064 .2015 Mathlib/Data/Fintype/Powerset.olean 65864 65864 .0000 Mathlib/Lean/Meta/Basic.olean 401520 65768 .8362 Mathlib/Geometry/Euclidean/Sphere/Power.olean 80176 65672 .1809 Mathlib/Analysis/Calculus/Deriv/Linear.olean 233552 65568 .7192 Mathlib/RingTheory/DedekindDomain/Dvr.olean 65472 65472 .0000 Mathlib/CategoryTheory/Thin.olean 210984 65248 .6907 Mathlib/Data/Set/Pointwise/ListOfFn.olean 92200 65088 .2940 Mathlib/RingTheory/EuclideanDomain.olean 233424 64880 .7220 Mathlib/GroupTheory/Archimedean.olean 64680 64680 .0000 Mathlib/Tactic/Monotonicity/Attr.olean 64672 64672 .0000 Mathlib/Lean/SMap.olean 134512 64368 .5214 Mathlib/LinearAlgebra/Matrix/AbsoluteValue.olean 81736 64216 .2143 Mathlib/Data/Nat/EvenOddRec.olean 89512 64200 .2827 Mathlib/Data/Finsupp/WellFounded.olean 87872 64144 .2700 Mathlib/Data/List/Palindrome.olean 262952 63912 .7569 Mathlib/Combinatorics/SimpleGraph/Acyclic.olean 63896 63896 .0000 Mathlib/Algebra/CharP/Pi.olean 84088 63696 .2425 Mathlib/Algebra/Order/Monoid/NatCast.olean 73440 63472 .1357 Mathlib/Data/Finite/Defs.olean 74328 62968 .1528 Mathlib/LinearAlgebra/FreeModule/Finite/Basic.olean 203096 62864 .6904 Mathlib/Topology/OmegaCompletePartialOrder.olean 100464 62832 .3745 Mathlib/Topology/Homotopy/Contractible.olean 98728 62808 .3638 Mathlib/Topology/Algebra/Order/ProjIcc.olean 64528 62744 .0276 Mathlib/CategoryTheory/Limits/Shapes/FiniteProducts.olean 113856 62712 .4491 Mathlib/Analysis/Calculus/Deriv/Star.olean 62544 62544 .0000 Mathlib/Lean/Exception.olean 215568 62472 .7101 Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.olean 63248 62344 .0142 Mathlib/Data/Equiv/Functor.olean 62904 62136 .0122 Mathlib/Init/ZeroOne.olean 118104 62112 .4740 Mathlib/Topology/IsLocallyHomeomorph.olean 261976 62112 .7629 Mathlib/Data/Nat/Factorization/PrimePow.olean 441608 62064 .8594 Mathlib/Topology/Sheaves/LocallySurjective.olean 206136 62040 .6990 Mathlib/RingTheory/Valuation/Integral.olean 244080 61816 .7467 Mathlib/Analysis/SpecialFunctions/NonIntegrable.olean 272128 61776 .7729 Mathlib/Analysis/NormedSpace/Ray.olean 94264 61744 .3449 Mathlib/LinearAlgebra/Matrix/MvPolynomial.olean 122112 61312 .4979 Mathlib/Analysis/Complex/ReImTopology.olean 110216 61208 .4446 Mathlib/Topology/Instances/Discrete.olean 270000 61136 .7735 Mathlib/Combinatorics/SimpleGraph/DegreeSum.olean 68080 60960 .1045 Mathlib/Order/Extension/Well.olean 79816 60824 .2379 Mathlib/Analysis/Complex/OperatorNorm.olean 280184 60792 .7830 Mathlib/Data/Rat/Floor.olean 86792 60728 .3003 Mathlib/Analysis/NormedSpace/DualNumber.olean 160400 60480 .6229 Mathlib/LinearAlgebra/FreeModule/Rank.olean 63528 60296 .0508 Mathlib/Algebra/Order/Monoid/ToMulBot.olean 100312 60296 .3989 Mathlib/Algebra/Divisibility/Units.olean 179456 60072 .6652 Mathlib/Algebra/Tropical/BigOperators.olean 64440 59944 .0697 Mathlib/Order/Filter/Curry.olean 95984 59912 .3758 Mathlib/Data/Vector/Zip.olean 61680 59784 .0307 Mathlib/Init/Data/Prod.olean 120056 59560 .5038 Mathlib/FieldTheory/Finiteness.olean 92208 59544 .3542 Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.olean 59832 59472 .0060 Mathlib/Data/Fintype/Sigma.olean 370544 59200 .8402 Mathlib/RingTheory/RootsOfUnity/Complex.olean 140440 59160 .5787 Mathlib/Combinatorics/SimpleGraph/Matching.olean 294624 59104 .7993 Mathlib/LinearAlgebra/Matrix/Polynomial.olean 167912 58952 .6489 Mathlib/Analysis/Calculus/Darboux.olean 90456 58736 .3506 Mathlib/Analysis/NormedSpace/Star/Exponential.olean 138216 58696 .5753 Mathlib/Data/Set/Equitable.olean 76800 58656 .2362 Mathlib/Algebra/Category/Ring/Instances.olean 58528 58528 .0000 Mathlib/CategoryTheory/Sites/AbelianSheaf.olean 111592 58480 .4759 Mathlib/RingTheory/MvPolynomial/Ideal.olean 123352 58272 .5275 Mathlib/Topology/QuasiSeparated.olean 237112 58248 .7543 Mathlib/Logic/Hydra.olean 59072 58120 .0161 Mathlib/Analysis/Normed/Group/Completion.olean 205064 58080 .7167 Mathlib/GroupTheory/CommutingProbability.olean 57936 57936 .0000 Mathlib/Data/Matrix/CharP.olean 57904 57904 .0000 Mathlib/CategoryTheory/Preadditive/Yoneda/Limits.olean 144984 57880 .6007 Mathlib/Data/List/Lemmas.olean 331800 57712 .8260 Mathlib/Analysis/Complex/OpenMapping.olean 321712 57504 .8212 Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.olean 59408 57440 .0331 Mathlib/Algebra/DirectSum/Finsupp.olean 63248 57328 .0935 Mathlib/Data/Nat/Units.olean 116160 57224 .5073 Mathlib/CategoryTheory/Limits/Constructions/EpiMono.olean 80496 57016 .2916 Mathlib/Order/ConditionallyCompleteLattice/Group.olean 138472 56976 .5885 Mathlib/Data/Polynomial/Induction.olean 1992472 56976 .9714 Mathlib/Algebra/GroupPower/Identities.olean 282560 56864 .7987 Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.olean 102832 56856 .4470 Mathlib/Topology/Algebra/Group/Compact.olean 310176 56856 .8166 Mathlib/Analysis/Normed/Order/UpperLower.olean 111904 56808 .4923 Mathlib/Data/Int/AbsoluteValue.olean 92200 56800 .3839 Mathlib/Analysis/Convex/PartitionOfUnity.olean 56624 56624 .0000 Mathlib/Data/DList/Instances.olean 57816 56544 .0220 Mathlib/Control/Monad/Basic.olean 146944 56400 .6161 Mathlib/MeasureTheory/Measure/Lebesgue/Integral.olean 140656 56336 .5994 Mathlib/Data/Real/Pointwise.olean 139112 56296 .5953 Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.olean 56288 56288 .0000 Mathlib/CategoryTheory/Category/RelCat.olean 203904 56280 .7239 Mathlib/Data/Fintype/Fin.olean 103288 56104 .4568 Mathlib/Geometry/Euclidean/Angle/Unoriented/Conformal.olean 115672 55832 .5173 Mathlib/Init/Data/Bool/Lemmas.olean 285704 55600 .8053 Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.olean 55864 55456 .0073 Mathlib/Algebra/Category/GroupCat/Preadditive.olean 157008 55248 .6481 Mathlib/Algebra/Module/DedekindDomain.olean 55192 55192 .0000 Mathlib/Control/SimpSet.olean 55632 55144 .0087 Mathlib/Combinatorics/Quiver/ConnectedComponent.olean 90784 55112 .3929 Mathlib/Analysis/Normed/Field/InfiniteSum.olean 89632 55016 .3862 Mathlib/Algebra/CharP/ExpChar.olean 120432 54952 .5437 Mathlib/Data/Finset/Finsupp.olean 100368 54928 .4527 Mathlib/Data/Finsupp/Fin.olean 65824 54784 .1677 Mathlib/Algebra/NeZero.olean 164976 54728 .6682 Mathlib/Data/Polynomial/CancelLeads.olean 100520 54656 .4562 Mathlib/Order/SuccPred/Relation.olean 158008 54584 .6545 Mathlib/Topology/Algebra/Order/T5.olean 129544 54504 .5792 Mathlib/Probability/Kernel/Invariance.olean 126216 54336 .5695 Mathlib/Order/Filter/IndicatorFunction.olean 63560 54232 .1467 Mathlib/Algebra/BigOperators/RingEquiv.olean 56808 53872 .0516 Mathlib/CategoryTheory/Adjunction/Over.olean 194752 53584 .7248 Mathlib/Analysis/SumIntegralComparisons.olean 70000 53408 .2370 Mathlib/LinearAlgebra/AffineSpace/MidpointZero.olean 84176 53296 .3668 Mathlib/Data/PNat/Interval.olean 198216 53032 .7324 Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.olean 155224 52976 .6587 Mathlib/Data/Polynomial/Monomial.olean 113856 52792 .5363 Mathlib/Algebra/Module/BigOperators.olean 83640 52680 .3701 Mathlib/Topology/UniformSpace/Matrix.olean 64368 52440 .1853 Mathlib/Data/Set/Intervals/Infinite.olean 373800 52376 .8598 Mathlib/Dynamics/Ergodic/AddCircle.olean 54208 52296 .0352 Mathlib/CategoryTheory/Monoidal/Types/Basic.olean 107888 52136 .5167 Mathlib/Analysis/Complex/Arg.olean 97544 52040 .4664 Mathlib/Topology/Sheaves/Limits.olean 99520 52016 .4773 Mathlib/GroupTheory/Subgroup/Saturated.olean 188584 51824 .7251 Mathlib/Topology/ContinuousFunction/Weierstrass.olean 155856 51544 .6692 Mathlib/LinearAlgebra/Multilinear/FiniteDimensional.olean 203448 51264 .7480 Mathlib/MeasureTheory/Measure/Sub.olean 122928 51248 .5831 Mathlib/Data/Set/Intervals/Monoid.olean 80512 51200 .3640 Mathlib/Algebra/Order/Sub/Basic.olean 114568 51168 .5533 Mathlib/Data/Int/Lemmas.olean 226248 50848 .7752 Mathlib/AlgebraicGeometry/PrimeSpectrum/Noetherian.olean 306656 50816 .8342 Mathlib/MeasureTheory/Group/AddCircle.olean 100640 50392 .4992 Mathlib/Algebra/GCDMonoid/Div.olean 274424 50352 .8165 Mathlib/Analysis/Analytic/Uniqueness.olean 54032 50272 .0695 Mathlib/Data/FunLike/Embedding.olean 50232 50232 .0000 Mathlib/CategoryTheory/Limits/Filtered.olean 275896 50200 .8180 Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.olean 247232 50080 .7974 Mathlib/Data/Nat/Choose/Factorization.olean 80512 49752 .3820 Mathlib/Tactic/Linarith/Lemmas.olean 146608 49744 .6607 Mathlib/Algebra/AlgebraicCard.olean 164104 49712 .6970 Mathlib/Data/Int/Units.olean 54872 49640 .0953 Mathlib/Data/Finset/Fin.olean 110128 49424 .5512 Mathlib/Topology/MetricSpace/Equicontinuity.olean 244312 49392 .7978 Mathlib/Analysis/NormedSpace/RieszLemma.olean 96264 49312 .4877 Mathlib/Init/Algebra/Functions.olean 229872 49144 .7862 Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.olean 446520 48976 .8903 Mathlib/NumberTheory/Fermat4.olean 116040 48856 .5789 Mathlib/Data/MvPolynomial/Polynomial.olean 157336 48840 .6895 Mathlib/Topology/Sheaves/PUnit.olean 48688 48688 .0000 Mathlib/Algebra/Order/Monoid/WithZero/Basic.olean 269616 48608 .8197 Mathlib/LinearAlgebra/Eigenspace/IsAlgClosed.olean 64408 48584 .2456 Mathlib/Data/Nat/Upto.olean 48256 48256 .0000 Mathlib/Logic/Equiv/MfldSimpsAttr.olean 134864 48168 .6428 Mathlib/CategoryTheory/Preadditive/Generator.olean 187848 48128 .7437 Mathlib/Combinatorics/SetFamily/HarrisKleitman.olean 118272 48104 .5932 Mathlib/Topology/Algebra/InfiniteSum/Real.olean 48064 48064 .0000 Mathlib/MeasureTheory/Integral/IntegralSimps.olean 48024 48024 .0000 Mathlib/Tactic/Qify/Attr.olean 48016 48016 .0000 Mathlib/Tactic/Zify/Attr.olean 48008 48008 .0000 Mathlib/Data/IsROrC/Attr.olean 91680 48008 .4763 Mathlib/MeasureTheory/Function/SpecialFunctions/IsROrC.olean 48000 48000 .0000 Mathlib/Data/TypeVec/Attr.olean 143688 47872 .6668 Mathlib/Data/Finset/PiInduction.olean 87120 47816 .4511 Mathlib/Topology/Sheaves/SheafOfFunctions.olean 253224 47816 .8111 Mathlib/MeasureTheory/Function/AEMeasurableOrder.olean 234416 47808 .7960 Mathlib/Analysis/Normed/Group/ControlledClosure.olean 47592 47592 .0000 Mathlib/MeasureTheory/Constructions/BorelSpace/Complex.olean 334064 47536 .8577 Mathlib/Topology/Category/TopCat/Limits/Cofiltered.olean 186112 47528 .7446 Mathlib/RingTheory/Nakayama.olean 95376 47208 .5050 Mathlib/Order/Monotone/Union.olean 115696 47064 .5932 Mathlib/Data/Nat/Dist.olean 78944 46992 .4047 Mathlib/GroupTheory/GroupAction/Support.olean 133080 46904 .6475 Mathlib/Order/Filter/ENNReal.olean 182168 46784 .7431 Mathlib/Data/Nat/Choose/Central.olean 102616 46768 .5442 Mathlib/Topology/ContinuousFunction/T0Sierpinski.olean 297592 46704 .8430 Mathlib/NumberTheory/Liouville/Basic.olean 67904 46696 .3123 Mathlib/Data/Set/Accumulate.olean 46648 46648 .0000 Mathlib/CategoryTheory/Preadditive/SingleObj.olean 77008 46632 .3944 Mathlib/Topology/Algebra/Order/LeftRight.olean 281528 46624 .8343 Mathlib/Topology/Instances/Complex.olean 47256 46592 .0140 Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.olean 57424 46512 .1900 Mathlib/CategoryTheory/Balanced.olean 51192 46368 .0942 Mathlib/Algebra/Hom/Equiv/Units/GroupWithZero.olean 356536 46184 .8704 Mathlib/Data/Polynomial/PartialFractions.olean 59432 46176 .2230 Mathlib/Analysis/NormedSpace/Extr.olean 90360 46120 .4895 Mathlib/Order/Bounds/OrderIso.olean 74720 46008 .3842 Mathlib/Init/CcLemmas.olean 84632 45920 .4574 Mathlib/Combinatorics/SimpleGraph/Metric.olean 76672 45848 .4020 Mathlib/Algebra/Hom/Commute.olean 46240 45800 .0095 Mathlib/Combinatorics/SimpleGraph/Ends/Properties.olean 89024 45776 .4858 Mathlib/Order/Partition/Equipartition.olean 150256 45760 .6954 Mathlib/Analysis/Subadditive.olean 105800 45560 .5693 Mathlib/MeasureTheory/Function/Floor.olean 49472 45528 .0797 Mathlib/CategoryTheory/Abelian/Injective.olean 82840 45448 .4513 Mathlib/CategoryTheory/Products/Bifunctor.olean 121344 45416 .6257 Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.olean 252944 44984 .8221 Mathlib/RingTheory/QuotientNilpotent.olean 44928 44928 .0000 Mathlib/Init/Align.olean 96920 44912 .5366 Mathlib/Order/ConditionallyCompleteLattice/Finset.olean 90608 44872 .5047 Mathlib/Data/Int/CharZero.olean 67304 44632 .3368 Mathlib/Data/Multiset/Range.olean 75336 44624 .4076 Mathlib/Algebra/Ring/Semiconj.olean 304984 44600 .8537 Mathlib/RingTheory/Prime.olean 73688 44560 .3952 Mathlib/Algebra/Order/Group/DenselyOrdered.olean 44496 44496 .0000 Mathlib/Data/KVMap.olean 104520 44408 .5751 Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.olean 183072 44384 .7575 Mathlib/NumberTheory/Liouville/Residual.olean 167552 44312 .7355 Mathlib/Analysis/Convex/StrictConvexBetween.olean 93776 44224 .5284 Mathlib/Algebra/Module/PointwisePi.olean 107184 44152 .5880 Mathlib/LinearAlgebra/Matrix/Nondegenerate.olean 107720 44080 .5907 Mathlib/Topology/Algebra/Order/ExtendFrom.olean 88944 44000 .5053 Mathlib/Analysis/Convex/Contractible.olean 128152 43992 .6567 Mathlib/Data/List/FinRange.olean 79472 43976 .4466 Mathlib/Data/Multiset/NatAntidiagonal.olean 326144 43896 .8654 Mathlib/LinearAlgebra/Charpoly/ToMatrix.olean 117664 43672 .6288 Mathlib/Topology/Algebra/Order/Archimedean.olean 141104 43384 .6925 Mathlib/Analysis/Convex/Measure.olean 46440 43256 .0685 Mathlib/Algebra/Order/ZeroLEOne.olean 43184 43184 .0000 Mathlib/Lean/LocalContext.olean 93600 43184 .5386 Mathlib/Topology/Algebra/Equicontinuity.olean 43176 43176 .0000 Mathlib/Mathport/Attributes.olean 115816 43048 .6283 Mathlib/Data/Nat/Cast/Field.olean 88856 42944 .5167 Mathlib/Topology/Partial.olean 214320 42808 .8002 Mathlib/Combinatorics/Additive/RuzsaCovering.olean 48216 42800 .1123 Mathlib/GroupTheory/GroupAction/BigOperators.olean 203192 42752 .7895 Mathlib/RingTheory/Polynomial/Hermite/Gaussian.olean 82560 42496 .4852 Mathlib/Data/Nat/Periodic.olean 126952 42456 .6655 Mathlib/Topology/ExtremallyDisconnected.olean 42400 42400 .0000 Mathlib/Tactic/ToLevel.olean 56072 42400 .2438 Mathlib/Logic/Pairwise.olean 113096 42296 .6260 Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.olean 62432 42248 .3232 Mathlib/Topology/Instances/Sign.olean 137760 42168 .6939 Mathlib/NumberTheory/ClassNumber/AdmissibleAbs.olean 42024 42024 .0000 Mathlib/Topology/Sheaves/Init.olean 95328 42016 .5592 Mathlib/Logic/Encodable/Lattice.olean 42008 42008 .0000 Mathlib/CategoryTheory/Category/Init.olean 42000 42000 .0000 Mathlib/Combinatorics/SimpleGraph/Init.olean 42000 42000 .0000 Mathlib/Tactic/Continuity/Init.olean 42000 42000 .0000 Mathlib/Tactic/Measurability/Init.olean 41992 41992 .0000 Mathlib/Data/Sym/Sym2/Init.olean 64472 41816 .3514 Mathlib/Algebra/Order/Invertible.olean 96112 41752 .5655 Mathlib/Topology/ExtendFrom.olean 51784 41616 .1963 Mathlib/Data/Rat/BigOperators.olean 59928 41512 .3073 Mathlib/Data/Set/Pointwise/Support.olean 88560 41400 .5325 Mathlib/Algebra/GroupWithZero/Commute.olean 51224 41192 .1958 Mathlib/Algebra/Category/ModuleCat/Simple.olean 694784 41104 .9408 Mathlib/RingTheory/DiscreteValuationRing/TFAE.olean 92720 40960 .5582 Mathlib/Data/Int/Order/Units.olean 55640 40904 .2648 Mathlib/Data/Finset/Order.olean 52120 40808 .2170 Mathlib/Data/Prod/PProd.olean 42008 40704 .0310 Mathlib/NumberTheory/Zsqrtd/ToReal.olean 41040 40680 .0087 Mathlib/Algebra/Group/Commutator.olean 122776 40600 .6693 Mathlib/Data/Set/Pointwise/Iterate.olean 67672 40592 .4001 Mathlib/Data/DList/Defs.olean 246512 40552 .8354 Mathlib/Data/MvPolynomial/Funext.olean 79384 40528 .4894 Mathlib/Algebra/BigOperators/NatAntidiagonal.olean 78920 40432 .4876 Mathlib/Logic/Lemmas.olean 40816 40424 .0096 Mathlib/Data/DList/Basic.olean 44760 40400 .0974 Mathlib/GroupTheory/Perm/ViaEmbedding.olean 586520 40200 .9314 Mathlib/RingTheory/Coprime/Ideal.olean 42272 40064 .0522 Mathlib/Data/Fintype/Parity.olean 64576 40024 .3802 Mathlib/Data/Fintype/Lattice.olean 43824 39968 .0879 Mathlib/LinearAlgebra/Matrix/Orthogonal.olean 66672 39848 .4023 Mathlib/Topology/FiberBundle/IsHomeomorphicTrivialBundle.olean 123248 39512 .6794 Mathlib/MeasureTheory/Integral/LebesgueNormedSpace.olean 101768 39464 .6122 Mathlib/Algebra/CharP/Quotient.olean 39416 39416 .0000 Mathlib/Init/Quot.olean 81560 39320 .5179 Mathlib/Data/Complex/Determinant.olean 154952 39288 .7464 Mathlib/NumberTheory/Wilson.olean 55856 39184 .2984 Mathlib/Data/Nat/Factorial/BigOperators.olean 154752 39176 .7468 Mathlib/LinearAlgebra/Multilinear/Basis.olean 63272 39056 .3827 Mathlib/CategoryTheory/Elementwise.olean 148664 39040 .7373 Mathlib/MeasureTheory/Decomposition/RadonNikodym.olean 211416 38728 .8168 Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.olean 39920 38592 .0332 Mathlib/Topology/Algebra/Module/Determinant.olean 68680 38552 .4386 Mathlib/Algebra/BigOperators/Multiset/Lemmas.olean 120600 38536 .6804 Mathlib/FieldTheory/AxGrothendieck.olean 99408 38496 .6127 Mathlib/FieldTheory/MvPolynomial.olean 216832 38104 .8242 Mathlib/Analysis/Convex/KreinMilman.olean 76896 38024 .5055 Mathlib/Algebra/GroupWithZero/Semiconj.olean 37864 37736 .0033 Mathlib/Algebra/PEmptyInstances.olean 196776 37664 .8085 Mathlib/Algebra/MonoidAlgebra/Ideal.olean 95456 37640 .6056 Mathlib/Data/Set/Intervals/SurjOn.olean 37600 37600 .0000 Mathlib/RingTheory/WittVector/WittAttributes.olean 118424 37600 .6824 Mathlib/Data/Real/Sign.olean 37560 37560 .0000 Mathlib/Data/Finsupp/Fintype.olean 56800 37440 .3408 Mathlib/MeasureTheory/Group/Pointwise.olean 49024 37248 .2402 Mathlib/Init/Data/Nat/GCD.olean 57320 37008 .3543 Mathlib/Algebra/BigOperators/Option.olean 154824 36920 .7615 Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.olean 340064 36832 .8916 Mathlib/MeasureTheory/Decomposition/UnsignedHahn.olean 585184 36640 .9373 Mathlib/Data/Complex/ExponentialBounds.olean 46784 36552 .2187 Mathlib/Data/String/Lemmas.olean 86728 36528 .5788 Mathlib/Data/Nat/Choose/Cast.olean 125504 36328 .7105 Mathlib/Data/Nat/WithBot.olean 45000 36312 .1930 Mathlib/Algebra/Order/Group/Bounds.olean 36088 36088 .0000 Mathlib/Lean/Message.olean 80080 36024 .5501 Mathlib/Analysis/Complex/Polynomial.olean 35920 35920 .0000 Mathlib/Lean/Linter.olean 133600 35896 .7313 Mathlib/NumberTheory/FrobeniusNumber.olean 58640 35816 .3892 Mathlib/SetTheory/ZFC/Ordinal.olean 35728 35728 .0000 Mathlib/Condensed/Abelian.olean 55872 35344 .3674 Mathlib/Data/Bool/AllAny.olean 35216 35216 .0000 Mathlib/Tactic.olean 35072 35072 .0000 Mathlib/Data/MvPolynomial/Invertible.olean 39336 35024 .1096 Mathlib/LinearAlgebra/FreeAlgebra.olean 121288 34992 .7114 Mathlib/MeasureTheory/Integral/ExpDecay.olean 183448 34888 .8098 Mathlib/Topology/Algebra/Semigroup.olean 99024 34760 .6489 Mathlib/Geometry/Euclidean/Sphere/Ptolemy.olean 55632 34568 .3786 Mathlib/Data/Rat/Sqrt.olean 207088 34520 .8333 Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.olean 51128 34496 .3253 Mathlib/Topology/Algebra/Module/Simple.olean 34392 34392 .0000 Mathlib/Lean/Elab/Tactic/Basic.olean 62992 34232 .4565 Mathlib/Order/Filter/ModEq.olean 49080 34216 .3028 Mathlib/Analysis/NormedSpace/IndicatorFunction.olean 34112 34112 .0000 Mathlib/Algebra/Order/Ring/CharZero.olean 33992 33992 .0000 Mathlib/Condensed/Basic.olean 48072 33952 .2937 Mathlib/Analysis/Calculus/Deriv/Support.olean 33936 33936 .0000 Mathlib/Util/Syntax.olean 106104 33912 .6803 Mathlib/RingTheory/Ideal/IdempotentFG.olean 33896 33896 .0000 Mathlib/Lean/Syntax.olean 54512 33832 .3793 Mathlib/Algebra/Regular/Pow.olean 74024 33792 .5434 Mathlib/Topology/Algebra/Order/ExtrClosure.olean 107200 33736 .6852 Mathlib/Algebra/Category/GroupCat/Zero.olean 63288 33696 .4675 Mathlib/Data/Fin/Tuple/BubbleSortInduction.olean 68440 33648 .5083 Mathlib/Data/Int/Div.olean 58000 33376 .4245 Mathlib/Order/Monotone/Odd.olean 52224 33320 .3619 Mathlib/Analysis/Calculus/AffineMap.olean 40224 33312 .1718 Mathlib/LinearAlgebra/FreeModule/Determinant.olean 74728 33280 .5546 Mathlib/Data/Int/Order/Lemmas.olean 102480 33264 .6754 Mathlib/Data/Set/BoolIndicator.olean 55216 33088 .4007 Mathlib/Analysis/NormedSpace/Int.olean 118736 32880 .7230 Mathlib/Data/Nat/Factorial/Cast.olean 34904 32816 .0598 Mathlib/Init/Data/Subtype/Basic.olean 61968 32736 .4717 Mathlib/Algebra/Order/Algebra.olean 80856 32592 .5969 Mathlib/Data/Int/Dvd/Basic.olean 32584 32584 .0000 Mathlib/CategoryTheory/Limits/Shapes/FunctorCategory.olean 43416 32496 .2515 Mathlib/Data/Int/Sqrt.olean 160416 32336 .7984 Mathlib/MeasureTheory/Covering/OneDim.olean 87912 32280 .6328 Mathlib/Data/Nat/Set.olean 189520 32120 .8305 Mathlib/RingTheory/RingHom/FiniteType.olean 86472 32056 .6292 Mathlib/Order/Monotone/Extension.olean 34024 31968 .0604 Mathlib/Data/FunLike/Fintype.olean 67920 31872 .5307 Mathlib/Data/Nat/PrimeFin.olean 172192 31480 .8171 Mathlib/Analysis/SpecialFunctions/Log/Monotone.olean 43504 31144 .2841 Mathlib/Data/Int/Dvd/Pow.olean 30944 30944 .0000 Mathlib/Util/DummyLabelAttr.olean 80312 30888 .6154 Mathlib/Algebra/Order/Field/Pi.olean 171816 30848 .8204 Mathlib/Combinatorics/SetFamily/Kleitman.olean 65512 30824 .5294 Mathlib/Data/MvPolynomial/Cardinal.olean 63512 30776 .5154 Mathlib/Data/W/Cardinal.olean 201512 30632 .8479 Mathlib/Probability/ConditionalExpectation.olean 39824 30608 .2314 Mathlib/Init/Data/Fin/Basic.olean 144320 30568 .7881 Mathlib/Algebra/CharP/CharAndCard.olean 56472 30520 .4595 Mathlib/Data/Int/Cast/Field.olean 45736 30256 .3384 Mathlib/Data/ZMod/Coprime.olean 124928 30192 .7583 Mathlib/NumberTheory/Basic.olean 37592 29952 .2032 Mathlib/Topology/Algebra/Order/Filter.olean 29840 29840 .0000 Mathlib/Logic/Small/List.olean 31632 29816 .0574 Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.olean 31264 29792 .0470 Mathlib/Data/ENat/Lattice.olean 46744 29768 .3631 Mathlib/Data/Int/NatPrime.olean 67288 29672 .5590 Mathlib/NumberTheory/LucasPrimality.olean 37976 29496 .2232 Mathlib/Analysis/Convex/Complex.olean 29296 29296 .0000 Mathlib/RingTheory/QuotientNoetherian.olean 47536 29208 .3855 Mathlib/Data/Nat/Choose/Bounds.olean 62864 29176 .5358 Mathlib/Order/ZornAtoms.olean 68048 29176 .5712 Mathlib/RingTheory/Localization/Cardinality.olean 49656 29144 .4130 Mathlib/Data/ZMod/Parity.olean 42632 28912 .3218 Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.olean 61056 28896 .5267 Mathlib/Init/Data/Ordering/Lemmas.olean 34376 28216 .1791 Mathlib/Init/Data/Nat/Basic.olean 48280 28192 .4160 Mathlib/RingTheory/ZMod.olean 116992 28144 .7594 Mathlib/RingTheory/RingHom/Finite.olean 40072 28096 .2988 Mathlib/CategoryTheory/Preadditive/Yoneda/Injective.olean 48424 28088 .4199 Mathlib/Algebra/Field/Power.olean 45016 27976 .3785 Mathlib/Topology/UniformSpace/CompleteSeparated.olean 27504 27504 .0000 Mathlib/Data/Countable/Small.olean 30928 27472 .1117 Mathlib/Init/Classical.olean 106512 27240 .7442 Mathlib/Combinatorics/Derangements/Exponential.olean 30912 27224 .1193 Mathlib/Algebra/Star/BigOperators.olean 44168 27144 .3854 Mathlib/Data/Polynomial/Cardinal.olean 59872 27080 .5477 Mathlib/RingTheory/RingHom/Integral.olean 27056 27056 .0000 Mathlib/CategoryTheory/Idempotents/SimplicialObject.olean 31408 27040 .1390 Mathlib/Geometry/Manifold/Metrizable.olean 37544 27008 .2806 Mathlib/Dynamics/FixedPoints/Topology.olean 32504 26984 .1698 Mathlib/CategoryTheory/Limits/EssentiallySmall.olean 35832 26976 .2471 Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.olean 40688 26864 .3397 Mathlib/Topology/Category/TopCat/EpiMono.olean 122856 26800 .7818 Mathlib/NumberTheory/PrimesCongruentOne.olean 43464 26784 .3837 Mathlib/Data/Nat/Choose/Dvd.olean 61464 26536 .5682 Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.olean 32104 26408 .1774 Mathlib/CategoryTheory/Limits/Shapes/Equivalence.olean 38992 26400 .3229 Mathlib/Data/Finsupp/Pwo.olean 46496 26216 .4361 Mathlib/Data/Nat/Choose/Vandermonde.olean 109184 26112 .7608 Mathlib/CategoryTheory/Abelian/Generator.olean 25976 25976 .0000 Mathlib/Data/Complex/Orientation.olean 37312 25968 .3040 Mathlib/Algebra/Order/Field/Canonical/Basic.olean 25936 25936 .0000 Mathlib/Tactic/Common.olean 32632 25680 .2130 Mathlib/Data/Bool/Set.olean 43976 25680 .4160 Mathlib/CategoryTheory/Groupoid/Basic.olean 25296 25296 .0000 Mathlib/Data/SetLike/Fintype.olean 25248 25248 .0000 Mathlib/Data/Fintype/Small.olean 114248 25216 .7792 Mathlib/Algebra/CharP/LocalRing.olean 29176 24976 .1439 Mathlib/Data/Finite/Set.olean 32376 24800 .2340 Mathlib/Order/UpperLower/LocallyFinite.olean 54232 24792 .5428 Mathlib/Analysis/SpecialFunctions/PolynomialExp.olean 24568 24568 .0000 Mathlib/Algebra/Category/GroupCat/Subobject.olean 26840 24560 .0849 Mathlib/MeasureTheory/Function/SpecialFunctions/Arctan.olean 24248 24248 .0000 Mathlib/Init/Data/Bool/Basic.olean 27192 24240 .1085 Mathlib/Data/Nat/GCD/BigOperators.olean 23704 23704 .0000 Mathlib/Tactic/Monotonicity/Lemmas.olean 35296 23400 .3370 Mathlib/Data/Complex/Cardinality.olean 23256 23256 .0000 Mathlib/Algebra/CharZero/Infinite.olean 24976 23144 .0733 Mathlib/RingTheory/Fintype.olean 23288 22960 .0140 Mathlib/Data/Nat/Cast/WithTop.olean 26408 22760 .1381 Mathlib/Init/Propext.olean 26104 22272 .1467 Mathlib/Init/Meta/WellFoundedTactics.olean 39880 22216 .4429 Mathlib/Init/IteSimp.olean 23264 22112 .0495 Mathlib/Tactic/Nontriviality.olean 21504 21504 .0000 Mathlib/Init/Data/Option/Lemmas.olean 42080 21120 .4980 Mathlib/Data/Int/Associated.olean 20600 20568 .0015 Mathlib/Data/Array/Basic.olean 20488 20488 .0000 Mathlib/Algebra/HierarchyDesign.olean 19904 19904 .0000 Mathlib/MeasureTheory/Tactic.olean 19752 19752 .0000 Mathlib/Lean/EnvExtension.olean 19472 19472 .0000 Mathlib/Topology/Tactic.olean 19424 19424 .0000 Mathlib/Data/Nat/PrimeNormNum.olean 19120 19120 .0000 Mathlib/Tactic/Positivity.olean 18864 18864 .0000 Mathlib/Data/Nat/SqrtNormNum.olean 18744 18576 .0089 Mathlib/Data/TypeMax.olean 18424 18424 .0000 Mathlib/Tactic/Linarith.olean 18400 18400 .0000 Mathlib/Tactic/Ring.olean 18360 18360 .0000 Mathlib/Tactic/NormNum.olean 18192 18192 .0000 Mathlib/Tactic/Monotonicity.olean 18008 18008 .0000 Mathlib/CategoryTheory/Functor/Default.olean 17784 17784 .0000 Mathlib/Tactic/NormCast.olean 15816 15816 .0000 Mathlib/Init/Data/Int/Lemmas.olean 15536 15536 .0000 Mathlib/Init/Data/Option/Basic.olean 15360 15360 .0000 Mathlib/Init/Data/Rat/Basic.olean 15192 15192 .0000 Mathlib/Init/Data/Int/DivMod.olean 12968 12968 .0000 Mathlib/Lean/Expr.olean 12648 12648 .0000 Mathlib/Init/Data/Option/Init/Lemmas.olean 12120 12120 .0000 Mathlib/Init/Classes/Order.olean 12064 12064 .0000 Mathlib/Init/Data/Nat/Div.olean