algebra/add_torsor.lean 4.01
algebra/algebra/basic.lean 30.92
algebra/algebra/bilinear.lean 5.35
algebra/algebra/operations.lean 12.91
algebra/algebra/ordered.lean 3.19
algebra/algebra/restrict_scalars.lean 2.94
algebra/algebra/subalgebra.lean 16.58
algebra/algebra/tower.lean 5.95
algebra/archimedean.lean 6.17
algebra/associated.lean 9.79
algebra/big_operators/basic.lean 25.74
algebra/big_operators/default.lean 2.39
algebra/big_operators/enat.lean 2.16
algebra/big_operators/fin.lean 2.26
algebra/big_operators/finprod.lean 16.08
algebra/big_operators/finsupp.lean 3.07
algebra/big_operators/intervals.lean 4.19
algebra/big_operators/nat_antidiagonal.lean 2.42
algebra/big_operators/order.lean 6.04
algebra/big_operators/pi.lean 2.97
algebra/big_operators/ring.lean 10.85
algebra/bounds.lean 2.68
algebra/category/Algebra/basic.lean 22.86
algebra/category/Algebra/limits.lean 8.82
algebra/category/CommRing/adjunctions.lean 3.73
algebra/category/CommRing/basic.lean 13.71
algebra/category/CommRing/colimits.lean 13.26
algebra/category/CommRing/default.lean 3.45
algebra/category/CommRing/filtered_colimits.lean 8.04
algebra/category/CommRing/limits.lean 27.08
algebra/category/CommRing/pushout.lean 10.12
algebra/category/FinVect.lean 10.96
algebra/category/Group/Z_Module_equivalence.lean 5.97
algebra/category/Group/abelian.lean 8.00
algebra/category/Group/adjunctions.lean 4.38
algebra/category/Group/basic.lean 12.44
algebra/category/Group/biproducts.lean 9.59
algebra/category/Group/colimits.lean 16.21
algebra/category/Group/default.lean 2.67
algebra/category/Group/filtered_colimits.lean 5.10
algebra/category/Group/images.lean 6.55
algebra/category/Group/limits.lean 23.93
algebra/category/Group/preadditive.lean 5.59
algebra/category/Group/subobject.lean 3.62
algebra/category/Group/zero.lean 3.21
algebra/category/Module/abelian.lean 14.71
algebra/category/Module/adjunctions.lean 41.32
algebra/category/Module/basic.lean 28.78
algebra/category/Module/colimits.lean 16.91
algebra/category/Module/epi_mono.lean 5.08
algebra/category/Module/filtered_colimits.lean 6.50
algebra/category/Module/kernels.lean 12.45
algebra/category/Module/limits.lean 24.99
algebra/category/Module/monoidal.lean 26.89
algebra/category/Module/projective.lean 8.47
algebra/category/Module/subobject.lean 7.33
algebra/category/Mon/adjunctions.lean 4.03
algebra/category/Mon/basic.lean 9.00
algebra/category/Mon/colimits.lean 7.38
algebra/category/Mon/default.lean 2.37
algebra/category/Mon/filtered_colimits.lean 13.85
algebra/category/Mon/limits.lean 8.35
algebra/category/Semigroup/basic.lean 10.25
algebra/char_p/algebra.lean 7.10
algebra/char_p/basic.lean 8.49
algebra/char_p/default.lean 3.98
algebra/char_p/exp_char.lean 3.12
algebra/char_p/invertible.lean 4.12
algebra/char_p/pi.lean 2.91
algebra/char_p/quotient.lean 3.00
algebra/char_p/subring.lean 2.96
algebra/char_zero.lean 3.20
algebra/continued_fractions/basic.lean 1.97
algebra/continued_fractions/computation/approximation_corollaries.lean 4.60
algebra/continued_fractions/computation/approximations.lean 18.03
algebra/continued_fractions/computation/basic.lean 2.47
algebra/continued_fractions/computation/correctness_terminating.lean 6.31
algebra/continued_fractions/computation/default.lean 2.62
algebra/continued_fractions/computation/terminates_iff_rat.lean 8.29
algebra/continued_fractions/computation/translations.lean 6.77
algebra/continued_fractions/continuants_recurrence.lean 1.82
algebra/continued_fractions/convergents_equiv.lean 6.97
algebra/continued_fractions/default.lean 2.63
algebra/continued_fractions/terminated_stable.lean 2.12
algebra/continued_fractions/translations.lean 2.34
algebra/covariant_and_contravariant.lean 0.93
algebra/default.lean 1.87
algebra/direct_limit.lean 40.26
algebra/direct_sum/algebra.lean 6.20
algebra/direct_sum/basic.lean 5.01
algebra/direct_sum/finsupp.lean 3.26
algebra/direct_sum/module.lean 3.88
algebra/direct_sum/ring.lean 14.08
algebra/divisibility.lean 1.18
algebra/euclidean_domain.lean 3.93
algebra/field.lean 3.26
algebra/field_power.lean 5.65
algebra/floor.lean 7.27
algebra/free.lean 5.06
algebra/free_algebra.lean 28.17
algebra/free_monoid.lean 3.05
algebra/free_non_unital_non_assoc_algebra.lean 4.04
algebra/gcd_monoid/basic.lean 7.92
algebra/gcd_monoid/finset.lean 3.90
algebra/gcd_monoid/multiset.lean 4.00
algebra/geom_sum.lean 5.76
algebra/group/basic.lean 2.32
algebra/group/commute.lean 0.92
algebra/group/conj.lean 2.77
algebra/group/default.lean 1.77
algebra/group/defs.lean 4.11
algebra/group/hom.lean 3.11
algebra/group/hom_instances.lean 7.53
algebra/group/inj_surj.lean 1.93
algebra/group/pi.lean 4.26
algebra/group/prod.lean 5.16
algebra/group/semiconj.lean 1.00
algebra/group/to_additive.lean 0.74
algebra/group/type_tags.lean 1.34
algebra/group/ulift.lean 1.81
algebra/group/units.lean 2.95
algebra/group/units_hom.lean 1.21
algebra/group/with_one.lean 1.91
algebra/group_action_hom.lean 4.08
algebra/group_power/basic.lean 3.89
algebra/group_power/default.lean 1.35
algebra/group_power/identities.lean 3.01
algebra/group_power/lemmas.lean 11.83
algebra/group_power/order.lean 3.08
algebra/group_ring_action.lean 3.19
algebra/group_with_zero/basic.lean 4.07
algebra/group_with_zero/default.lean 0.68
algebra/group_with_zero/defs.lean 1.23
algebra/group_with_zero/power.lean 3.56
algebra/hierarchy_design.lean 0.30
algebra/homology/additive.lean 55.87
algebra/homology/augment.lean 33.93
algebra/homology/complex_shape.lean 0.87
algebra/homology/differential_object.lean 31.55
algebra/homology/exact.lean 11.52
algebra/homology/flip.lean 38.01
algebra/homology/functor.lean 4.64
algebra/homology/homological_complex.lean 61.18
algebra/homology/homology.lean 15.00
algebra/homology/homotopy.lean 47.45
algebra/homology/homotopy_category.lean 7.93
algebra/homology/image_to_kernel.lean 39.86
algebra/homology/quasi_iso.lean 3.11
algebra/homology/single.lean 38.58
algebra/indicator_function.lean 7.46
algebra/invertible.lean 1.95
algebra/iterate_hom.lean 2.40
algebra/lattice_ordered_group.lean 4.32
algebra/lie/abelian.lean 20.48
algebra/lie/base_change.lean 10.50
algebra/lie/basic.lean 19.33
algebra/lie/cartan_matrix.lean 7.20
algebra/lie/cartan_subalgebra.lean 5.52
algebra/lie/character.lean 4.95
algebra/lie/classical.lean 32.17
algebra/lie/direct_sum.lean 18.03
algebra/lie/free.lean 13.36
algebra/lie/ideal_operations.lean 9.29
algebra/lie/matrix.lean 17.07
algebra/lie/nilpotent.lean 9.44
algebra/lie/non_unital_non_assoc_algebra.lean 2.75
algebra/lie/of_associative.lean 8.82
algebra/lie/quotient.lean 6.14
algebra/lie/semisimple.lean 4.83
algebra/lie/skew_adjoint.lean 24.55
algebra/lie/solvable.lean 7.51
algebra/lie/subalgebra.lean 19.44
algebra/lie/submodule.lean 21.85
algebra/lie/tensor_product.lean 25.30
algebra/lie/universal_enveloping.lean 24.65
algebra/lie/weights.lean 38.79
algebra/linear_recurrence.lean 22.41
algebra/module/basic.lean 5.89
algebra/module/default.lean 2.20
algebra/module/hom.lean 4.15
algebra/module/linear_map.lean 6.39
algebra/module/opposites.lean 2.29
algebra/module/ordered.lean 2.80
algebra/module/pi.lean 3.06
algebra/module/pointwise_pi.lean 2.43
algebra/module/prod.lean 2.01
algebra/module/projective.lean 31.50
algebra/module/submodule.lean 5.46
algebra/module/submodule_lattice.lean 7.90
algebra/module/submodule_pointwise.lean 3.22
algebra/module/ulift.lean 5.25
algebra/monoid_algebra/basic.lean 75.48
algebra/monoid_algebra/to_direct_sum.lean 4.69
algebra/non_unital_alg_hom.lean 4.89
algebra/opposites.lean 2.43
algebra/order/absolute_value.lean 2.85
algebra/order/basic.lean 1.22
algebra/order/euclidean_absolute_value.lean 1.36
algebra/order/field.lean 7.51
algebra/order/functions.lean 0.88
algebra/order/group.lean 10.60
algebra/order/monoid.lean 10.12
algebra/order/monoid_lemmas.lean 1.45
algebra/order/pi.lean 2.00
algebra/order/pointwise.lean 4.22
algebra/order/ring.lean 16.31
algebra/order/smul.lean 2.40
algebra/order/sub.lean 3.48
algebra/order/with_zero.lean 3.86
algebra/pempty_instances.lean 2.17
algebra/periodic.lean 7.67
algebra/pointwise.lean 8.25
algebra/polynomial/big_operators.lean 21.72
algebra/polynomial/group_ring_action.lean 5.73
algebra/punit_instances.lean 2.46
algebra/quadratic_discriminant.lean 6.18
algebra/quandle.lean 14.69
algebra/quaternion.lean 33.36
algebra/quaternion_basis.lean 11.89
algebra/regular/basic.lean 1.29
algebra/regular/pow.lean 1.52
algebra/regular/smul.lean 1.81
algebra/ring/basic.lean 6.61
algebra/ring/boolean_ring.lean 3.93
algebra/ring/comp_typeclasses.lean 1.42
algebra/ring/default.lean 0.93
algebra/ring/pi.lean 2.18
algebra/ring/prod.lean 1.80
algebra/ring/ulift.lean 1.59
algebra/ring_quot.lean 36.03
algebra/smul_with_zero.lean 2.37
algebra/squarefree.lean 9.33
algebra/star/algebra.lean 2.53
algebra/star/basic.lean 2.64
algebra/star/chsh.lean 19.58
algebra/star/pi.lean 1.91
algebra/support.lean 5.00
algebra/triv_sq_zero_ext.lean 4.03
algebra/tropical/basic.lean 2.34
algebraic_geometry/EllipticCurve.lean 2.41
algebraic_geometry/Scheme.lean 9.61
algebraic_geometry/Spec.lean 10.58
algebraic_geometry/is_open_comap_C.lean 4.07
algebraic_geometry/locally_ringed_space.lean 20.66
algebraic_geometry/presheafed_space.lean 23.67
algebraic_geometry/presheafed_space/has_colimits.lean 55.92
algebraic_geometry/prime_spectrum.lean 10.95
algebraic_geometry/sheafed_space.lean 4.92
algebraic_geometry/stalks.lean 15.46
algebraic_geometry/structure_sheaf.lean 33.44
algebraic_topology/Moore_complex.lean 22.54
algebraic_topology/cech_nerve.lean 115.03
algebraic_topology/simplex_category.lean 42.02
algebraic_topology/simplicial_object.lean 72.64
algebraic_topology/simplicial_set.lean 9.72
algebraic_topology/topological_simplex.lean 15.22
analysis/ODE/gronwall.lean 8.29
analysis/analytic/basic.lean 51.62
analysis/analytic/composition.lean 55.32
analysis/analytic/inverse.lean 63.76
analysis/analytic/linear.lean 15.76
analysis/analytic/radius_liminf.lean 6.86
analysis/asymptotics/asymptotic_equivalent.lean 10.87
analysis/asymptotics/asymptotics.lean 24.58
analysis/asymptotics/specific_asymptotics.lean 5.73
analysis/calculus/conformal/inner_product.lean 6.37
analysis/calculus/conformal/normed_space.lean 4.55
analysis/calculus/darboux.lean 8.80
analysis/calculus/deriv.lean 69.70
analysis/calculus/extend_deriv.lean 18.21
analysis/calculus/fderiv.lean 90.29
analysis/calculus/fderiv_analytic.lean 5.14
analysis/calculus/fderiv_measurable.lean 23.88
analysis/calculus/fderiv_symmetric.lean 29.17
analysis/calculus/formal_multilinear_series.lean 5.70
analysis/calculus/implicit.lean 30.72
analysis/calculus/inverse.lean 22.18
analysis/calculus/iterated_deriv.lean 24.97
analysis/calculus/lagrange_multipliers.lean 17.67
analysis/calculus/lhopital.lean 11.00
analysis/calculus/local_extr.lean 14.24
analysis/calculus/mean_value.lean 24.00
analysis/calculus/parametric_integral.lean 17.47
analysis/calculus/specific_functions.lean 26.97
analysis/calculus/tangent_cone.lean 14.68
analysis/calculus/times_cont_diff.lean 114.04
analysis/complex/basic.lean 16.11
analysis/complex/circle.lean 12.86
analysis/complex/conformal.lean 21.22
analysis/complex/isometry.lean 25.60
analysis/complex/polynomial.lean 13.86
analysis/complex/real_deriv.lean 15.58
analysis/complex/roots_of_unity.lean 12.09
analysis/complex/upper_half_plane.lean 22.38
analysis/convex/basic.lean 13.72
analysis/convex/caratheodory.lean 7.01
analysis/convex/combination.lean 11.37
analysis/convex/complex.lean 4.31
analysis/convex/cone.lean 18.33
analysis/convex/exposed.lean 5.73
analysis/convex/extrema.lean 6.40
analysis/convex/extreme.lean 3.96
analysis/convex/function.lean 26.62
analysis/convex/independent.lean 5.87
analysis/convex/integral.lean 11.37
analysis/convex/specific_functions/exp_log.lean 10.51
analysis/convex/specific_functions/pow.lean 14.12
analysis/convex/topology.lean 11.26
analysis/fourier.lean 28.24
analysis/hofer.lean 6.09
analysis/inner_product_space/basic.lean 129.19
analysis/inner_product_space/calculus.lean 12.37
analysis/inner_product_space/conformal_linear_map.lean 7.14
analysis/inner_product_space/euclidean_dist.lean 7.88
analysis/inner_product_space/projection.lean 91.78
analysis/mean_inequalities.lean 14.77
analysis/mean_inequalities_exp.lean 29.95
analysis/normed_space/SemiNormedGroup.lean 14.73
analysis/normed_space/SemiNormedGroup/kernels.lean 12.75
analysis/normed_space/add_torsor.lean 12.36
analysis/normed_space/affine_isometry.lean 11.45
analysis/normed_space/banach.lean 12.18
analysis/normed_space/basic.lean 52.66
analysis/normed_space/bounded_linear_maps.lean 46.70
analysis/normed_space/complemented.lean 7.31
analysis/normed_space/conformal_linear_map.lean 7.17
analysis/normed_space/dual.lean 35.61
analysis/normed_space/enorm.lean 16.66
analysis/normed_space/exponential.lean 14.64
analysis/normed_space/exponential_calculus.lean 9.05
analysis/normed_space/extend.lean 11.60
analysis/normed_space/finite_dimension.lean 46.09
analysis/normed_space/hahn_banach.lean 16.23
analysis/normed_space/indicator_function.lean 4.31
analysis/normed_space/int.lean 4.30
analysis/normed_space/linear_isometry.lean 5.31
analysis/normed_space/mazur_ulam.lean 12.26
analysis/normed_space/multilinear.lean 111.47
analysis/normed_space/normed_group_hom.lean 17.67
analysis/normed_space/normed_group_hom_completion.lean 12.33
analysis/normed_space/normed_group_quotient.lean 20.12
analysis/normed_space/operator_norm.lean 84.40
analysis/normed_space/ordered.lean 4.38
analysis/normed_space/pi_Lp.lean 39.72
analysis/normed_space/riesz_lemma.lean 6.03
analysis/normed_space/units.lean 22.46
analysis/normed_space/weak_dual.lean 6.61
analysis/p_series.lean 16.70
analysis/quaternion.lean 14.77
analysis/seminorm.lean 5.75
analysis/special_functions/arsinh.lean 5.18
analysis/special_functions/bernstein.lean 22.31
analysis/special_functions/complex/arg.lean 26.18
analysis/special_functions/complex/log.lean 28.16
analysis/special_functions/complex/log_calculus.lean 9.36
analysis/special_functions/exp_log.lean 9.91
analysis/special_functions/exp_log_calculus.lean 19.83
analysis/special_functions/integrals.lean 47.65
analysis/special_functions/polynomials.lean 10.34
analysis/special_functions/pow.lean 79.03
analysis/special_functions/pow_calculus.lean 40.93
analysis/special_functions/sqrt.lean 8.43
analysis/special_functions/trigonometric/arctan.lean 17.80
analysis/special_functions/trigonometric/arctan_calculus.lean 12.42
analysis/special_functions/trigonometric/basic.lean 53.15
analysis/special_functions/trigonometric/basic_calculus.lean 19.48
analysis/special_functions/trigonometric/chebyshev.lean 6.53
analysis/special_functions/trigonometric/complex.lean 19.02
analysis/special_functions/trigonometric/complex_calculus.lean 7.27
analysis/special_functions/trigonometric/inverse.lean 12.64
analysis/special_functions/trigonometric/inverse_calculus.lean 10.55
analysis/specific_limits.lean 29.38
category_theory/Fintype.lean 5.80
category_theory/abelian/basic.lean 23.04
category_theory/abelian/diagram_lemmas/four.lean 5.58
category_theory/abelian/exact.lean 17.82
category_theory/abelian/ext.lean 7.99
category_theory/abelian/non_preadditive.lean 18.99
category_theory/abelian/opposite.lean 20.90
category_theory/abelian/projective.lean 9.33
category_theory/abelian/pseudoelements.lean 11.42
category_theory/action.lean 4.97
category_theory/additive/basic.lean 2.49
category_theory/adjunction/adjoint_functor_theorems.lean 2.04
category_theory/adjunction/basic.lean 19.55
category_theory/adjunction/comma.lean 7.41
category_theory/adjunction/default.lean 1.87
category_theory/adjunction/fully_faithful.lean 16.78
category_theory/adjunction/lifting.lean 3.53
category_theory/adjunction/limits.lean 39.21
category_theory/adjunction/mates.lean 10.79
category_theory/adjunction/opposites.lean 16.92
category_theory/adjunction/over.lean 2.47
category_theory/adjunction/reflective.lean 5.37
category_theory/arrow.lean 5.04
category_theory/category/Cat.lean 2.53
category_theory/category/Groupoid.lean 2.25
category_theory/category/Kleisli.lean 1.62
category_theory/category/Quiv.lean 2.86
category_theory/category/Rel.lean 2.31
category_theory/category/default.lean 2.74
category_theory/category/pairwise.lean 6.88
category_theory/category/preorder.lean 3.04
category_theory/category/ulift.lean 9.50
category_theory/closed/cartesian.lean 9.61
category_theory/closed/functor.lean 12.29
category_theory/closed/ideal.lean 8.77
category_theory/closed/monoidal.lean 2.51
category_theory/closed/types.lean 8.30
category_theory/closed/zero.lean 3.41
category_theory/comma.lean 25.58
category_theory/concrete_category/basic.lean 1.94
category_theory/concrete_category/bundled.lean 1.30
category_theory/concrete_category/bundled_hom.lean 3.50
category_theory/concrete_category/default.lean 1.53
category_theory/concrete_category/reflects_isomorphisms.lean 1.83
category_theory/concrete_category/unbundled_hom.lean 1.61
category_theory/conj.lean 2.82
category_theory/connected_components.lean 2.26
category_theory/const.lean 5.26
category_theory/core.lean 3.06
category_theory/currying.lean 16.65
category_theory/derived.lean 17.79
category_theory/differential_object.lean 39.28
category_theory/discrete_category.lean 3.44
category_theory/elements.lean 19.59
category_theory/endomorphism.lean 2.29
category_theory/enriched/basic.lean 31.16
category_theory/epi_mono.lean 2.86
category_theory/eq_to_hom.lean 3.06
category_theory/equivalence.lean 11.23
category_theory/essential_image.lean 2.17
category_theory/essentially_small.lean 15.20
category_theory/filtered.lean 40.24
category_theory/fin_category.lean 2.30
category_theory/full_subcategory.lean 1.99
category_theory/fully_faithful.lean 3.65
category_theory/functor.lean 2.17
category_theory/functor_category.lean 3.86
category_theory/functorial.lean 1.54
category_theory/graded_object.lean 14.74
category_theory/grothendieck.lean 9.32
category_theory/groupoid.lean 2.37
category_theory/hom_functor.lean 2.68
category_theory/is_connected.lean 2.36
category_theory/isomorphism.lean 7.65
category_theory/isomorphism_classes.lean 2.16
category_theory/lifting_properties.lean 4.86
category_theory/limits/colimit_limit.lean 5.79
category_theory/limits/comma.lean 13.56
category_theory/limits/concrete_category.lean 4.95
category_theory/limits/cones.lean 89.37
category_theory/limits/connected.lean 4.96
category_theory/limits/constructions/binary_products.lean 2.26
category_theory/limits/constructions/epi_mono.lean 2.06
category_theory/limits/constructions/equalizers.lean 6.27
category_theory/limits/constructions/finite_products_of_binary_products.lean 7.13
category_theory/limits/constructions/limits_of_products_and_equalizers.lean 22.46
category_theory/limits/constructions/over/connected.lean 12.89
category_theory/limits/constructions/over/default.lean 2.35
category_theory/limits/constructions/over/products.lean 23.87
category_theory/limits/constructions/pullbacks.lean 6.67
category_theory/limits/constructions/weakly_initial.lean 1.86
category_theory/limits/creates.lean 5.81
category_theory/limits/filtered_colimit_commutes_finite_limit.lean 11.28
category_theory/limits/final.lean 45.44
category_theory/limits/fubini.lean 10.94
category_theory/limits/functor_category.lean 13.26
category_theory/limits/has_limits.lean 28.67
category_theory/limits/is_limit.lean 25.19
category_theory/limits/kan_extension.lean 26.83
category_theory/limits/lattice.lean 3.77
category_theory/limits/opposites.lean 3.35
category_theory/limits/over.lean 21.41
category_theory/limits/pi.lean 2.46
category_theory/limits/preserves/basic.lean 11.96
category_theory/limits/preserves/filtered.lean 2.52
category_theory/limits/preserves/functor_category.lean 2.68
category_theory/limits/preserves/limits.lean 3.79
category_theory/limits/preserves/shapes/binary_products.lean 4.08
category_theory/limits/preserves/shapes/equalizers.lean 3.52
category_theory/limits/preserves/shapes/products.lean 2.74
category_theory/limits/preserves/shapes/pullbacks.lean 4.78
category_theory/limits/preserves/shapes/terminal.lean 1.92
category_theory/limits/presheaf.lean 10.45
category_theory/limits/punit.lean 3.91
category_theory/limits/shapes/binary_products.lean 45.34
category_theory/limits/shapes/biproducts.lean 101.10
category_theory/limits/shapes/concrete_category.lean 2.05
category_theory/limits/shapes/default.lean 2.35
category_theory/limits/shapes/disjoint_coproduct.lean 2.03
category_theory/limits/shapes/equalizers.lean 26.10
category_theory/limits/shapes/finite_limits.lean 5.47
category_theory/limits/shapes/finite_products.lean 2.26
category_theory/limits/shapes/images.lean 24.85
category_theory/limits/shapes/kernel_pair.lean 2.82
category_theory/limits/shapes/kernels.lean 49.11
category_theory/limits/shapes/normal_mono.lean 7.90
category_theory/limits/shapes/products.lean 4.03
category_theory/limits/shapes/pullbacks.lean 26.74
category_theory/limits/shapes/reflexive.lean 2.30
category_theory/limits/shapes/regular_mono.lean 5.69
category_theory/limits/shapes/split_coequalizer.lean 2.60
category_theory/limits/shapes/strict_initial.lean 2.18
category_theory/limits/shapes/strong_epi.lean 2.71
category_theory/limits/shapes/terminal.lean 7.28
category_theory/limits/shapes/types.lean 17.93
category_theory/limits/shapes/wide_equalizers.lean 24.42
category_theory/limits/shapes/wide_pullbacks.lean 43.05
category_theory/limits/shapes/zero.lean 14.40
category_theory/limits/small_complete.lean 3.07
category_theory/limits/types.lean 14.37
category_theory/limits/yoneda.lean 4.38
category_theory/linear/default.lean 7.78
category_theory/linear/linear_functor.lean 5.39
category_theory/linear/yoneda.lean 16.74
category_theory/monad/adjunction.lean 33.41
category_theory/monad/algebra.lean 21.06
category_theory/monad/basic.lean 18.97
category_theory/monad/coequalizer.lean 5.25
category_theory/monad/default.lean 1.95
category_theory/monad/equiv_mon.lean 40.26
category_theory/monad/kleisli.lean 5.32
category_theory/monad/limits.lean 12.71
category_theory/monad/monadicity.lean 9.61
category_theory/monad/products.lean 17.64
category_theory/monad/types.lean 4.21
category_theory/monoidal/CommMon_.lean 31.79
category_theory/monoidal/End.lean 11.80
category_theory/monoidal/Mod.lean 6.86
category_theory/monoidal/Mon_.lean 34.09
category_theory/monoidal/braided.lean 6.81
category_theory/monoidal/category.lean 11.10
category_theory/monoidal/center.lean 21.53
category_theory/monoidal/discrete.lean 3.06
category_theory/monoidal/free/basic.lean 5.16
category_theory/monoidal/free/coherence.lean 10.60
category_theory/monoidal/functor.lean 8.57
category_theory/monoidal/functor_category.lean 5.47
category_theory/monoidal/functorial.lean 2.76
category_theory/monoidal/internal/Module.lean 39.78
category_theory/monoidal/internal/functor_category.lean 60.38
category_theory/monoidal/internal/limits.lean 9.01
category_theory/monoidal/internal/types.lean 25.68
category_theory/monoidal/limits.lean 5.66
category_theory/monoidal/natural_transformation.lean 9.62
category_theory/monoidal/of_chosen_finite_products.lean 33.45
category_theory/monoidal/of_has_finite_products.lean 10.31
category_theory/monoidal/opposite.lean 4.80
category_theory/monoidal/preadditive.lean 3.71
category_theory/monoidal/rigid.lean 4.91
category_theory/monoidal/skeleton.lean 2.14
category_theory/monoidal/tor.lean 3.90
category_theory/monoidal/transport.lean 18.77
category_theory/monoidal/types.lean 11.52
category_theory/natural_isomorphism.lean 3.92
category_theory/natural_transformation.lean 2.07
category_theory/opposites.lean 14.52
category_theory/over.lean 22.93
category_theory/path_category.lean 2.25
category_theory/pempty.lean 1.52
category_theory/pi/basic.lean 13.61
category_theory/preadditive/Mat.lean 72.92
category_theory/preadditive/additive_functor.lean 8.47
category_theory/preadditive/biproducts.lean 55.03
category_theory/preadditive/default.lean 6.52
category_theory/preadditive/functor_category.lean 6.20
category_theory/preadditive/opposite.lean 8.43
category_theory/preadditive/projective.lean 12.30
category_theory/preadditive/projective_resolution.lean 18.82
category_theory/preadditive/schur.lean 8.87
category_theory/preadditive/single_obj.lean 2.39
category_theory/products/associator.lean 4.07
category_theory/products/basic.lean 9.44
category_theory/products/bifunctor.lean 1.65
category_theory/products/default.lean 1.51
category_theory/punit.lean 2.95
category_theory/quotient.lean 3.34
category_theory/reflects_isomorphisms.lean 1.83
category_theory/shift.lean 1.93
category_theory/sigma/basic.lean 4.54
category_theory/simple.lean 3.22
category_theory/single_obj.lean 4.72
category_theory/sites/canonical.lean 6.78
category_theory/sites/closed.lean 7.35
category_theory/sites/grothendieck.lean 6.91
category_theory/sites/pretopology.lean 5.02
category_theory/sites/sheaf.lean 19.40
category_theory/sites/sheaf_of_types.lean 29.75
category_theory/sites/sieves.lean 14.48
category_theory/sites/spaces.lean 3.01
category_theory/sites/types.lean 9.11
category_theory/skeletal.lean 4.87
category_theory/structured_arrow.lean 15.25
category_theory/subobject/basic.lean 26.25
category_theory/subobject/default.lean 2.51
category_theory/subobject/factor_thru.lean 9.66
category_theory/subobject/lattice.lean 26.01
category_theory/subobject/limits.lean 24.95
category_theory/subobject/mono_over.lean 15.88
category_theory/subobject/types.lean 4.64
category_theory/subobject/well_powered.lean 2.50
category_theory/subterminal.lean 10.80
category_theory/sums/associator.lean 4.38
category_theory/sums/basic.lean 4.95
category_theory/sums/default.lean 1.51
category_theory/thin.lean 1.83
category_theory/triangulated/basic.lean 10.68
category_theory/triangulated/pretriangulated.lean 4.42
category_theory/triangulated/rotate.lean 58.46
category_theory/types.lean 3.48
category_theory/whiskering.lean 7.86
category_theory/with_terminal.lean 35.51
category_theory/yoneda.lean 15.44
combinatorics/choose/bounds.lean 1.84
combinatorics/colex.lean 5.25
combinatorics/composition.lean 16.27
combinatorics/derangements/basic.lean 5.63
combinatorics/derangements/exponential.lean 7.29
combinatorics/derangements/finite.lean 4.16
combinatorics/hales_jewett.lean 3.79
combinatorics/hall.lean 7.32
combinatorics/partition.lean 2.80
combinatorics/pigeonhole.lean 3.34
combinatorics/quiver.lean 2.15
combinatorics/simple_graph/adj_matrix.lean 8.68
combinatorics/simple_graph/basic.lean 7.22
combinatorics/simple_graph/degree_sum.lean 7.22
combinatorics/simple_graph/matching.lean 2.02
combinatorics/simple_graph/strongly_regular.lean 2.41
combinatorics/simple_graph/subgraph.lean 3.59
computability/DFA.lean 2.72
computability/NFA.lean 5.24
computability/encoding.lean 2.24
computability/epsilon_NFA.lean 2.57
computability/halting.lean 6.29
computability/language.lean 2.77
computability/partrec.lean 13.58
computability/partrec_code.lean 22.30
computability/primrec.lean 16.91
computability/reduce.lean 3.67
computability/regular_expressions.lean 17.90
computability/tm_computable.lean 4.71
computability/tm_to_partrec.lean 32.51
computability/turing_machine.lean 35.34
control/applicative.lean 1.37
control/basic.lean 0.83
control/bifunctor.lean 0.89
control/bitraversable/basic.lean 0.56
control/bitraversable/instances.lean 2.28
control/bitraversable/lemmas.lean 0.78
control/equiv_functor.lean 2.27
control/equiv_functor/instances.lean 7.62
control/fix.lean 2.18
control/fold.lean 5.81
control/functor.lean 0.70
control/functor/multivariate.lean 1.33
control/lawful_fix.lean 4.88
control/monad/basic.lean 0.90
control/monad/cont.lean 3.16
control/monad/writer.lean 1.60
control/traversable/basic.lean 0.83
control/traversable/default.lean 1.39
control/traversable/derive.lean 1.94
control/traversable/equiv.lean 2.57
control/traversable/instances.lean 5.17
control/traversable/lemmas.lean 1.12
control/ulift.lean 0.44
control/uliftable.lean 0.98
data/W/basic.lean 2.75
data/W/cardinal.lean 2.73
data/analysis/filter.lean 11.14
data/analysis/topology.lean 6.12
data/array/lemmas.lean 3.39
data/bitvec/basic.lean 6.59
data/bitvec/core.lean 2.47
data/bool.lean 1.11
data/bracket.lean 0.30
data/buffer/basic.lean 4.69
data/buffer/parser/basic.lean 41.32
data/buffer/parser/numeral.lean 2.70
data/bundle.lean 1.93
data/char.lean 0.37
data/complex/basic.lean 43.62
data/complex/exponential.lean 75.16
data/complex/exponential_bounds.lean 23.45
data/complex/is_R_or_C.lean 149.63
data/complex/module.lean 28.17
data/dfinsupp.lean 60.74
data/dlist/basic.lean 0.30
data/dlist/instances.lean 1.74
data/equiv/basic.lean 15.32
data/equiv/denumerable.lean 5.53
data/equiv/embedding.lean 3.38
data/equiv/encodable/basic.lean 3.31
data/equiv/encodable/lattice.lean 2.31
data/equiv/encodable/small.lean 1.56
data/equiv/fin.lean 7.97
data/equiv/fintype.lean 5.37
data/equiv/functor.lean 1.29
data/equiv/list.lean 5.01
data/equiv/local_equiv.lean 5.37
data/equiv/module.lean 4.95
data/equiv/mul_add.lean 4.68
data/equiv/mul_add_aut.lean 3.88
data/equiv/nat.lean 1.70
data/equiv/option.lean 3.21
data/equiv/ring.lean 2.56
data/equiv/ring_aut.lean 1.83
data/equiv/transfer_instance.lean 19.20
data/erased.lean 1.18
data/fin.lean 22.34
data/fin2.lean 0.40
data/fin_enum.lean 5.74
data/finmap.lean 5.73
data/finset/basic.lean 33.74
data/finset/default.lean 1.88
data/finset/fold.lean 2.97
data/finset/intervals.lean 4.06
data/finset/lattice.lean 6.78
data/finset/nat_antidiagonal.lean 2.46
data/finset/noncomm_prod.lean 5.44
data/finset/order.lean 1.64
data/finset/pi.lean 2.28
data/finset/pi_induction.lean 2.48
data/finset/pimage.lean 2.96
data/finset/powerset.lean 3.76
data/finset/preimage.lean 3.64
data/finset/sort.lean 3.60
data/finsupp/antidiagonal.lean 5.73
data/finsupp/basic.lean 57.47
data/finsupp/default.lean 2.29
data/finsupp/lattice.lean 3.60
data/finsupp/pointwise.lean 3.37
data/finsupp/to_dfinsupp.lean 6.84
data/fintype/basic.lean 25.48
data/fintype/card.lean 9.49
data/fintype/card_embedding.lean 3.21
data/fintype/fin.lean 2.35
data/fintype/intervals.lean 2.32
data/fintype/list.lean 2.47
data/fintype/small.lean 2.04
data/fintype/sort.lean 2.14
data/fp/basic.lean 3.05
data/hash_map.lean 12.98
data/holor.lean 6.11
data/int/absolute_value.lean 4.81
data/int/basic.lean 10.26
data/int/cast.lean 6.29
data/int/char_zero.lean 1.90
data/int/gcd.lean 4.82
data/int/least_greatest.lean 1.40
data/int/modeq.lean 2.83
data/int/nat_prime.lean 1.86
data/int/order.lean 3.15
data/int/parity.lean 4.27
data/int/range.lean 1.66
data/int/sqrt.lean 1.32
data/lazy_list.lean 0.49
data/lazy_list/basic.lean 5.09
data/list/alist.lean 3.29
data/list/bag_inter.lean 2.31
data/list/basic.lean 40.31
data/list/chain.lean 3.00
data/list/cycle.lean 10.51
data/list/default.lean 1.57
data/list/defs.lean 0.92
data/list/duplicate.lean 2.23
data/list/erase_dup.lean 1.57
data/list/forall2.lean 3.00
data/list/func.lean 3.33
data/list/indexes.lean 3.19
data/list/intervals.lean 2.75
data/list/lex.lean 1.79
data/list/min_max.lean 8.49
data/list/nat_antidiagonal.lean 2.08
data/list/nodup.lean 3.31
data/list/nodup_equiv_fin.lean 6.22
data/list/of_fn.lean 2.46
data/list/pairwise.lean 3.64
data/list/palindrome.lean 1.59
data/list/perm.lean 11.23
data/list/range.lean 3.11
data/list/rotate.lean 6.91
data/list/sections.lean 1.54
data/list/sigma.lean 11.86
data/list/sort.lean 4.29
data/list/sublists.lean 3.20
data/list/tfae.lean 1.66
data/list/zip.lean 6.87
data/matrix/basic.lean 31.32
data/matrix/basis.lean 8.12
data/matrix/block.lean 33.72
data/matrix/char_p.lean 3.77
data/matrix/dmatrix.lean 3.99
data/matrix/hadamard.lean 3.87
data/matrix/kronecker.lean 7.18
data/matrix/notation.lean 19.44
data/matrix/pequiv.lean 9.71
data/mllist.lean 0.43
data/multiset/antidiagonal.lean 3.56
data/multiset/basic.lean 24.93
data/multiset/default.lean 1.61
data/multiset/erase_dup.lean 2.19
data/multiset/finset_ops.lean 3.20
data/multiset/fold.lean 4.27
data/multiset/functor.lean 4.55
data/multiset/intervals.lean 1.74
data/multiset/lattice.lean 2.98
data/multiset/nat_antidiagonal.lean 1.69
data/multiset/nodup.lean 2.80
data/multiset/pi.lean 3.99
data/multiset/powerset.lean 4.43
data/multiset/range.lean 1.65
data/multiset/sections.lean 2.89
data/multiset/sort.lean 1.50
data/mv_polynomial/basic.lean 53.35
data/mv_polynomial/cardinal.lean 4.01
data/mv_polynomial/comap.lean 4.44
data/mv_polynomial/comm_ring.lean 5.71
data/mv_polynomial/counit.lean 3.08
data/mv_polynomial/default.lean 2.86
data/mv_polynomial/equiv.lean 16.07
data/mv_polynomial/expand.lean 7.44
data/mv_polynomial/funext.lean 8.98
data/mv_polynomial/invertible.lean 4.20
data/mv_polynomial/monad.lean 20.12
data/mv_polynomial/pderiv.lean 18.65
data/mv_polynomial/rename.lean 18.20
data/mv_polynomial/supported.lean 9.81
data/mv_polynomial/variables.lean 19.92
data/nat/basic.lean 9.52
data/nat/bitwise.lean 4.83
data/nat/cast.lean 3.82
data/nat/choose/basic.lean 2.92
data/nat/choose/cast.lean 3.66
data/nat/choose/default.lean 2.72
data/nat/choose/dvd.lean 2.17
data/nat/choose/sum.lean 5.41
data/nat/choose/vandermonde.lean 4.26
data/nat/digits.lean 10.84
data/nat/dist.lean 1.82
data/nat/enat.lean 6.35
data/nat/factorial/basic.lean 2.85
data/nat/factorial/cast.lean 3.44
data/nat/fib.lean 3.49
data/nat/gcd.lean 2.60
data/nat/lattice.lean 3.18
data/nat/log.lean 2.30
data/nat/modeq.lean 6.00
data/nat/mul_ind.lean 3.66
data/nat/multiplicity.lean 13.82
data/nat/pairing.lean 3.14
data/nat/parity.lean 4.26
data/nat/pow.lean 2.90
data/nat/prime.lean 9.38
data/nat/psub.lean 1.82
data/nat/sqrt.lean 2.88
data/nat/totient.lean 9.38
data/nat/upto.lean 1.52
data/nat/with_bot.lean 1.79
data/num/basic.lean 0.62
data/num/bitwise.lean 1.85
data/num/lemmas.lean 22.66
data/num/prime.lean 2.81
data/opposite.lean 0.84
data/option/basic.lean 2.43
data/option/defs.lean 0.55
data/ordmap/ordnode.lean 2.39
data/ordmap/ordset.lean 23.17
data/part.lean 2.47
data/pequiv.lean 15.33
data/pfun.lean 3.65
data/pfunctor/multivariate/M.lean 15.34
data/pfunctor/multivariate/W.lean 2.91
data/pfunctor/multivariate/basic.lean 3.39
data/pfunctor/univariate/M.lean 6.18
data/pfunctor/univariate/basic.lean 2.73
data/pfunctor/univariate/default.lean 1.83
data/pi.lean 0.78
data/pnat/basic.lean 2.59
data/pnat/factors.lean 3.80
data/pnat/intervals.lean 2.29
data/pnat/prime.lean 3.11
data/pnat/xgcd.lean 3.83
data/polynomial/algebra_map.lean 15.48
data/polynomial/basic.lean 39.93
data/polynomial/cancel_leads.lean 4.96
data/polynomial/cardinal.lean 3.48
data/polynomial/coeff.lean 10.77
data/polynomial/default.lean 3.00
data/polynomial/degree/card_pow_degree.lean 7.97
data/polynomial/degree/default.lean 2.71
data/polynomial/degree/definitions.lean 20.01
data/polynomial/degree/lemmas.lean 4.44
data/polynomial/degree/trailing_degree.lean 5.85
data/polynomial/denoms_clearable.lean 4.09
data/polynomial/derivative.lean 20.72
data/polynomial/div.lean 12.85
data/polynomial/erase_lead.lean 5.05
data/polynomial/eval.lean 37.09
data/polynomial/field_division.lean 28.93
data/polynomial/hasse_deriv.lean 12.09
data/polynomial/identities.lean 8.19
data/polynomial/induction.lean 5.16
data/polynomial/inductions.lean 8.24
data/polynomial/integral_normalization.lean 12.25
data/polynomial/iterated_deriv.lean 8.54
data/polynomial/lifts.lean 7.00
data/polynomial/mirror.lean 5.26
data/polynomial/monic.lean 13.06
data/polynomial/monomial.lean 9.69
data/polynomial/reverse.lean 5.95
data/polynomial/ring_division.lean 16.54
data/polynomial/taylor.lean 5.55
data/pprod.lean 0.30
data/prod.lean 0.83
data/qpf/multivariate/basic.lean 3.50
data/qpf/multivariate/constructions/cofix.lean 6.06
data/qpf/multivariate/constructions/comp.lean 3.74
data/qpf/multivariate/constructions/const.lean 2.28
data/qpf/multivariate/constructions/fix.lean 3.90
data/qpf/multivariate/constructions/prj.lean 2.16
data/qpf/multivariate/constructions/quot.lean 2.17
data/qpf/multivariate/constructions/sigma.lean 3.47
data/qpf/multivariate/default.lean 1.89
data/qpf/univariate/basic.lean 5.60
data/quot.lean 0.60
data/rat/basic.lean 12.30
data/rat/cast.lean 8.18
data/rat/default.lean 1.90
data/rat/denumerable.lean 2.43
data/rat/floor.lean 4.80
data/rat/meta_defs.lean 1.57
data/rat/order.lean 3.39
data/rat/sqrt.lean 1.46
data/real/basic.lean 11.34
data/real/cardinality.lean 7.64
data/real/cau_seq.lean 10.61
data/real/cau_seq_completion.lean 6.46
data/real/conjugate_exponents.lean 3.65
data/real/ennreal.lean 57.04
data/real/ereal.lean 15.61
data/real/golden_ratio.lean 13.93
data/real/hyperreal.lean 21.32
data/real/irrational.lean 12.28
data/real/nnreal.lean 15.39
data/real/pi/bounds.lean 14.28
data/real/pi/leibniz.lean 14.34
data/real/pi/wallis.lean 15.80
data/real/sign.lean 2.79
data/real/sqrt.lean 6.14
data/rel.lean 2.57
data/semiquot.lean 2.56
data/seq/computation.lean 3.36
data/seq/parallel.lean 6.66
data/seq/seq.lean 8.06
data/seq/wseq.lean 19.13
data/set/Union_lift.lean 1.65
data/set/accumulate.lean 1.41
data/set/basic.lean 17.09
data/set/bool.lean 0.74
data/set/constructions.lean 6.05
data/set/countable.lean 3.50
data/set/default.lean 1.95
data/set/enumerate.lean 2.55
data/set/finite.lean 8.87
data/set/function.lean 3.30
data/set/intervals/basic.lean 15.61
data/set/intervals/default.lean 1.93
data/set/intervals/disjoint.lean 1.50
data/set/intervals/image_preimage.lean 13.10
data/set/intervals/infinite.lean 2.46
data/set/intervals/ord_connected.lean 2.67
data/set/intervals/pi.lean 4.35
data/set/intervals/proj_Icc.lean 1.78
data/set/intervals/surj_on.lean 1.90
data/set/intervals/unordered_interval.lean 4.90
data/set/lattice.lean 11.05
data/set/pairwise.lean 1.83
data/set_like/basic.lean 0.90
data/set_like/fintype.lean 1.78
data/setoid/basic.lean 2.46
data/setoid/partition.lean 2.83
data/sigma/basic.lean 0.74
data/sigma/default.lean 0.45
data/stream/basic.lean 1.81
data/string/basic.lean 2.26
data/string/defs.lean 0.37
data/subtype.lean 0.56
data/sum.lean 0.66
data/sym/basic.lean 3.57
data/sym/card.lean 3.05
data/sym/sym2.lean 23.51
data/tprod.lean 2.52
data/tree.lean 0.38
data/typevec.lean 2.73
data/ulift.lean 0.77
data/vector/basic.lean 6.96
data/vector/zip.lean 2.10
data/vector3.lean 0.83
data/zmod/algebra.lean 3.05
data/zmod/basic.lean 24.40
data/zmod/parity.lean 3.84
data/zmod/quotient.lean 3.65
deprecated/group.lean 1.64
deprecated/ring.lean 1.62
deprecated/subfield.lean 2.92
deprecated/subgroup.lean 8.11
deprecated/submonoid.lean 3.59
deprecated/subring.lean 2.74
dynamics/circle/rotation_number/translation_number.lean 27.06
dynamics/ergodic/conservative.lean 10.62
dynamics/ergodic/measure_preserving.lean 8.13
dynamics/fixed_points/basic.lean 0.94
dynamics/fixed_points/topology.lean 2.64
dynamics/flow.lean 3.62
dynamics/omega_limit.lean 6.57
dynamics/periodic_pts.lean 3.14
field_theory/abel_ruffini.lean 15.71
field_theory/adjoin.lean 32.11
field_theory/chevalley_warning.lean 7.75
field_theory/finite/basic.lean 17.29
field_theory/finite/galois_field.lean 11.97
field_theory/finite/polynomial.lean 13.83
field_theory/finiteness.lean 5.38
field_theory/fixed.lean 26.68
field_theory/galois.lean 34.27
field_theory/intermediate_field.lean 11.55
field_theory/is_alg_closed/algebraic_closure.lean 20.99
field_theory/is_alg_closed/basic.lean 20.46
field_theory/minpoly.lean 19.08
field_theory/mv_polynomial.lean 5.13
field_theory/normal.lean 13.68
field_theory/perfect_closure.lean 11.48
field_theory/polynomial_galois_group.lean 25.64
field_theory/primitive_element.lean 15.17
field_theory/separable.lean 24.21
field_theory/separable_degree.lean 5.37
field_theory/splitting_field.lean 40.65
field_theory/subfield.lean 8.26
field_theory/tower.lean 6.34
geometry/euclidean/basic.lean 63.19
geometry/euclidean/circumcenter.lean 70.35
geometry/euclidean/default.lean 5.28
geometry/euclidean/monge_point.lean 53.47
geometry/euclidean/sphere.lean 13.36
geometry/euclidean/triangle.lean 21.89
geometry/manifold/algebra/left_invariant_derivation.lean 41.94
geometry/manifold/algebra/lie_group.lean 6.43
geometry/manifold/algebra/monoid.lean 8.56
geometry/manifold/algebra/smooth_functions.lean 10.15
geometry/manifold/algebra/structures.lean 6.53
geometry/manifold/basic_smooth_bundle.lean 27.95
geometry/manifold/bump_function.lean 9.29
geometry/manifold/charted_space.lean 9.25
geometry/manifold/conformal_groupoid.lean 4.65
geometry/manifold/derivation_bundle.lean 15.61
geometry/manifold/diffeomorph.lean 13.99
geometry/manifold/instances/real.lean 15.98
geometry/manifold/instances/sphere.lean 53.02
geometry/manifold/instances/units_of_normed_algebra.lean 5.81
geometry/manifold/local_invariant_properties.lean 19.80
geometry/manifold/mfderiv.lean 48.55
geometry/manifold/partition_of_unity.lean 12.30
geometry/manifold/smooth_manifold_with_corners.lean 19.13
geometry/manifold/times_cont_mdiff.lean 85.31
geometry/manifold/times_cont_mdiff_map.lean 6.57
geometry/manifold/whitney_embedding.lean 10.43
group_theory/abelianization.lean 3.39
group_theory/archimedean.lean 2.96
group_theory/complement.lean 5.57
group_theory/congruence.lean 6.55
group_theory/coset.lean 8.35
group_theory/eckmann_hilton.lean 0.85
group_theory/finiteness.lean 3.41
group_theory/free_abelian_group.lean 9.20
group_theory/free_abelian_group_finsupp.lean 4.07
group_theory/free_group.lean 18.54
group_theory/free_product.lean 9.45
group_theory/general_commutator.lean 3.22
group_theory/group_action/basic.lean 5.52
group_theory/group_action/default.lean 2.12
group_theory/group_action/defs.lean 2.08
group_theory/group_action/group.lean 2.53
group_theory/group_action/prod.lean 1.31
group_theory/group_action/sub_mul_action.lean 3.27
group_theory/group_action/units.lean 1.15
group_theory/index.lean 2.59
group_theory/is_free_group.lean 5.94
group_theory/monoid_localization.lean 23.47
group_theory/nielsen_schreier.lean 5.51
group_theory/nilpotent.lean 6.78
group_theory/order_of_element.lean 14.77
group_theory/p_group.lean 7.17
group_theory/perm/basic.lean 7.00
group_theory/perm/concrete_cycle.lean 10.91
group_theory/perm/cycle_type.lean 15.60
group_theory/perm/cycles.lean 32.41
group_theory/perm/fin.lean 40.09
group_theory/perm/list.lean 12.29
group_theory/perm/option.lean 8.20
group_theory/perm/sign.lean 18.53
group_theory/perm/subgroup.lean 2.26
group_theory/perm/support.lean 16.89
group_theory/presented_group.lean 2.92
group_theory/quotient_group.lean 16.08
group_theory/semidirect_product.lean 28.28
group_theory/solvable.lean 7.16
group_theory/specific_groups/alternating.lean 10.53
group_theory/specific_groups/cyclic.lean 21.79
group_theory/specific_groups/dihedral.lean 5.49
group_theory/specific_groups/quaternion.lean 8.68
group_theory/subgroup/basic.lean 36.30
group_theory/subgroup/pointwise.lean 2.82
group_theory/submonoid/basic.lean 3.50
group_theory/submonoid/center.lean 2.04
group_theory/submonoid/default.lean 1.98
group_theory/submonoid/membership.lean 6.13
group_theory/submonoid/operations.lean 6.50
group_theory/submonoid/pointwise.lean 2.67
group_theory/sylow.lean 12.37
linear_algebra/adic_completion.lean 8.83
linear_algebra/affine_space/affine_equiv.lean 19.39
linear_algebra/affine_space/affine_map.lean 17.85
linear_algebra/affine_space/affine_subspace.lean 13.22
linear_algebra/affine_space/basic.lean 1.94
linear_algebra/affine_space/combination.lean 26.83
linear_algebra/affine_space/finite_dimensional.lean 10.39
linear_algebra/affine_space/independent.lean 21.20
linear_algebra/affine_space/midpoint.lean 4.30
linear_algebra/affine_space/ordered.lean 10.65
linear_algebra/alternating.lean 71.19
linear_algebra/basic.lean 75.28
linear_algebra/basis.lean 65.42
linear_algebra/bilinear_form.lean 79.54
linear_algebra/bilinear_map.lean 4.01
linear_algebra/charpoly.lean 16.54
linear_algebra/clifford_algebra/basic.lean 27.84
linear_algebra/clifford_algebra/conjugation.lean 45.90
linear_algebra/clifford_algebra/default.lean 5.03
linear_algebra/clifford_algebra/equivs.lean 41.97
linear_algebra/coevaluation.lean 11.89
linear_algebra/contraction.lean 4.90
linear_algebra/default.lean 2.51
linear_algebra/determinant.lean 23.80
linear_algebra/dfinsupp.lean 16.59
linear_algebra/dimension.lean 31.56
linear_algebra/direct_sum/finsupp.lean 19.23
linear_algebra/direct_sum/tensor_product.lean 11.87
linear_algebra/dual.lean 52.45
linear_algebra/eigenspace.lean 34.46
linear_algebra/exterior_algebra.lean 26.75
linear_algebra/finite_dimensional.lean 58.79
linear_algebra/finsupp.lean 51.27
linear_algebra/finsupp_vector_space.lean 15.54
linear_algebra/free_algebra.lean 6.99
linear_algebra/free_module.lean 5.44
linear_algebra/free_module_pid.lean 30.46
linear_algebra/invariant_basis_number.lean 13.98
linear_algebra/isomorphisms.lean 6.54
linear_algebra/lagrange.lean 7.83
linear_algebra/linear_independent.lean 45.69
linear_algebra/linear_pmap.lean 8.71
linear_algebra/matrix/absolute_value.lean 4.77
linear_algebra/matrix/basis.lean 9.47
linear_algebra/matrix/block.lean 13.52
linear_algebra/matrix/charpoly/basic.lean 11.09
linear_algebra/matrix/charpoly/coeff.lean 29.97
linear_algebra/matrix/circulant.lean 6.83
linear_algebra/matrix/default.lean 4.27
linear_algebra/matrix/determinant.lean 62.55
linear_algebra/matrix/diagonal.lean 15.43
linear_algebra/matrix/dot_product.lean 2.90
linear_algebra/matrix/dual.lean 5.95
linear_algebra/matrix/finite_dimensional.lean 3.95
linear_algebra/matrix/fpow.lean 13.20
linear_algebra/matrix/is_diag.lean 4.67
linear_algebra/matrix/nonsingular_inverse.lean 30.20
linear_algebra/matrix/orthogonal.lean 2.97
linear_algebra/matrix/polynomial.lean 14.05
linear_algebra/matrix/reindex.lean 6.95
linear_algebra/matrix/symmetric.lean 3.33
linear_algebra/matrix/to_lin.lean 57.14
linear_algebra/matrix/to_linear_equiv.lean 13.13
linear_algebra/matrix/trace.lean 4.26
linear_algebra/matrix/transvection.lean 57.99
linear_algebra/multilinear/basic.lean 70.14
linear_algebra/multilinear/tensor_product.lean 9.83
linear_algebra/pi.lean 25.32
linear_algebra/pi_tensor_product.lean 47.66
linear_algebra/prod.lean 43.76
linear_algebra/projection.lean 21.07
linear_algebra/quadratic_form.lean 93.12
linear_algebra/quotient.lean 12.97
linear_algebra/sesquilinear_form.lean 9.15
linear_algebra/smodeq.lean 3.25
linear_algebra/special_linear_group.lean 7.03
linear_algebra/std_basis.lean 21.50
linear_algebra/tensor_algebra.lean 23.07
linear_algebra/tensor_product.lean 48.65
linear_algebra/tensor_product_basis.lean 4.07
linear_algebra/trace.lean 5.62
linear_algebra/unitary_group.lean 6.85
linear_algebra/vandermonde.lean 15.72
logic/basic.lean 1.58
logic/embedding.lean 3.38
logic/function/basic.lean 1.06
logic/function/conjugate.lean 0.43
logic/function/iterate.lean 0.54
logic/is_empty.lean 0.45
logic/nontrivial.lean 0.96
logic/relation.lean 1.42
logic/relator.lean 0.35
logic/small.lean 1.04
logic/unique.lean 0.77
measure_theory/category/Meas.lean 7.73
measure_theory/constructions/borel_space.lean 37.63
measure_theory/constructions/pi.lean 47.21
measure_theory/constructions/prod.lean 54.51
measure_theory/decomposition/jordan.lean 19.39
measure_theory/decomposition/lebesgue.lean 53.72
measure_theory/decomposition/radon_nikodym.lean 10.34
measure_theory/decomposition/signed_hahn.lean 16.50
measure_theory/decomposition/unsigned_hahn.lean 16.53
measure_theory/function/ae_eq_fun.lean 11.03
measure_theory/function/ae_eq_of_integral.lean 13.86
measure_theory/function/ae_measurable_sequence.lean 6.19
measure_theory/function/conditional_expectation.lean 69.57
measure_theory/function/continuous_map_dense.lean 25.50
measure_theory/function/ess_sup.lean 6.83
measure_theory/function/l1_space.lean 54.16
measure_theory/function/l2_space.lean 27.18
measure_theory/function/lp_space.lean 150.99
measure_theory/function/simple_func_dense.lean 71.63
measure_theory/function/special_functions.lean 6.79
measure_theory/function/strongly_measurable.lean 11.85
measure_theory/group/arithmetic.lean 11.30
measure_theory/group/basic.lean 19.45
measure_theory/group/prod.lean 16.95
measure_theory/integral/bochner.lean 72.77
measure_theory/integral/integrable_on.lean 14.03
measure_theory/integral/integral_eq_improper.lean 8.95
measure_theory/integral/interval_integral.lean 92.76
measure_theory/integral/lebesgue.lean 141.71
measure_theory/integral/mean_inequalities.lean 17.38
measure_theory/integral/set_integral.lean 40.37
measure_theory/integral/set_to_l1.lean 52.69
measure_theory/integral/vitali_caratheodory.lean 32.21
measure_theory/measurable_space.lean 23.03
measure_theory/measurable_space_def.lean 3.82
measure_theory/measure/content.lean 18.51
measure_theory/measure/finite_measure_weak_convergence.lean 8.61
measure_theory/measure/giry_monad.lean 15.35
measure_theory/measure/haar.lean 29.09
measure_theory/measure/haar_lebesgue.lean 34.33
measure_theory/measure/hausdorff.lean 40.57
measure_theory/measure/lebesgue.lean 40.44
measure_theory/measure/measure_space.lean 85.58
measure_theory/measure/measure_space_def.lean 11.26
measure_theory/measure/outer_measure.lean 56.41
measure_theory/measure/regular.lean 15.79
measure_theory/measure/stieltjes.lean 20.39
measure_theory/measure/vector_measure.lean 43.81
measure_theory/measure/with_density_vector_measure.lean 10.99
measure_theory/pi_system.lean 5.05
measure_theory/probability_mass_function.lean 30.99
measure_theory/tactic.lean 3.89
meta/coinductive_predicates.lean 0.92
meta/expr.lean 1.04
meta/expr_lens.lean 0.42
meta/rb_map.lean 0.41
meta/uchange.lean 0.33
model_theory/basic.lean 7.17
number_theory/ADE_inequality.lean 9.19
number_theory/arithmetic_function.lean 48.50
number_theory/basic.lean 2.92
number_theory/bernoulli.lean 60.46
number_theory/bernoulli_polynomials.lean 16.96
number_theory/class_number/admissible_abs.lean 5.04
number_theory/class_number/admissible_absolute_value.lean 7.26
number_theory/class_number/admissible_card_pow_degree.lean 15.34
number_theory/class_number/finite.lean 35.62
number_theory/dioph.lean 10.90
number_theory/divisors.lean 5.29
number_theory/fermat4.lean 7.61
number_theory/function_field.lean 11.95
number_theory/l_series.lean 11.93
number_theory/liouville/basic.lean 7.48
number_theory/liouville/liouville_constant.lean 8.66
number_theory/lucas_lehmer.lean 25.13
number_theory/number_field.lean 8.34
number_theory/padics/default.lean 4.14
number_theory/padics/hensel.lean 31.30
number_theory/padics/padic_integers.lean 36.39
number_theory/padics/padic_norm.lean 30.84
number_theory/padics/padic_numbers.lean 53.90
number_theory/padics/ring_homs.lean 39.07
number_theory/pell.lean 10.01
number_theory/primes_congruent_one.lean 8.82
number_theory/primorial.lean 10.72
number_theory/pythagorean_triples.lean 25.91
number_theory/quadratic_reciprocity.lean 59.07
number_theory/sum_four_squares.lean 28.74
number_theory/sum_two_squares.lean 5.41
number_theory/zsqrtd/basic.lean 15.78
number_theory/zsqrtd/gaussian_int.lean 36.63
number_theory/zsqrtd/to_real.lean 4.26
order/atoms.lean 5.47
order/basic.lean 1.54
order/boolean_algebra.lean 10.49
order/bounded_lattice.lean 5.80
order/bounds.lean 2.89
order/category/LinearOrder.lean 2.35
order/category/NonemptyFinLinOrd.lean 2.69
order/category/PartialOrder.lean 2.36
order/category/Preorder.lean 2.37
order/category/omega_complete_partial_order.lean 4.77
order/closure.lean 2.54
order/compactly_generated.lean 5.92
order/complete_boolean_algebra.lean 3.48
order/complete_lattice.lean 7.62
order/conditionally_complete_lattice.lean 10.19
order/copy.lean 3.24
order/countable_dense_linear_order.lean 9.17
order/default.lean 1.17
order/directed.lean 1.00
order/disjointed.lean 2.74
order/extension.lean 1.90
order/filter/archimedean.lean 3.17
order/filter/at_top_bot.lean 10.12
order/filter/bases.lean 8.38
order/filter/basic.lean 21.67
order/filter/cofinite.lean 3.75
order/filter/countable_Inter.lean 2.85
order/filter/default.lean 2.02
order/filter/ennreal.lean 5.04
order/filter/extr.lean 2.94
order/filter/filter_product.lean 3.22
order/filter/germ.lean 7.03
order/filter/indicator_function.lean 2.94
order/filter/interval.lean 3.24
order/filter/lift.lean 5.73
order/filter/partial.lean 4.09
order/filter/pointwise.lean 3.91
order/filter/ultrafilter.lean 4.42
order/fixed_points.lean 1.61
order/galois_connection.lean 2.88
order/ideal.lean 4.52
order/iterate.lean 2.07
order/lattice.lean 2.66
order/lattice_intervals.lean 1.74
order/lexicographic.lean 1.73
order/liminf_limsup.lean 5.17
order/modular_lattice.lean 2.17
order/omega_complete_partial_order.lean 8.69
order/ord_continuous.lean 3.12
order/order_dual.lean 0.81
order/order_iso_nat.lean 3.93
order/partial_sups.lean 2.69
order/pfilter.lean 2.07
order/pilex.lean 1.82
order/preorder_hom.lean 4.13
order/prime_ideal.lean 2.77
order/rel_classes.lean 1.17
order/rel_iso.lean 4.55
order/semiconj_Sup.lean 4.60
order/symm_diff.lean 2.03
order/well_founded.lean 1.01
order/well_founded_set.lean 7.48
order/zorn.lean 2.32
probability_theory/independence.lean 5.66
probability_theory/integration.lean 7.52
representation_theory/maschke.lean 7.60
ring_theory/adjoin/basic.lean 7.79
ring_theory/adjoin/default.lean 2.61
ring_theory/adjoin/fg.lean 6.06
ring_theory/adjoin/polynomial.lean 5.80
ring_theory/adjoin/power_basis.lean 6.46
ring_theory/adjoin_root.lean 9.05
ring_theory/algebra_tower.lean 24.80
ring_theory/algebraic.lean 10.17
ring_theory/artinian.lean 20.94
ring_theory/class_group.lean 20.29
ring_theory/coprime.lean 3.43
ring_theory/dedekind_domain.lean 52.56
ring_theory/derivation.lean 13.38
ring_theory/discrete_valuation_ring.lean 9.86
ring_theory/eisenstein_criterion.lean 5.33
ring_theory/euclidean_domain.lean 3.83
ring_theory/finiteness.lean 26.77
ring_theory/fintype.lean 2.15
ring_theory/flat.lean 5.12
ring_theory/fractional_ideal.lean 38.49
ring_theory/free_comm_ring.lean 11.25
ring_theory/free_ring.lean 2.58
ring_theory/hahn_series.lean 86.90
ring_theory/ideal/basic.lean 12.82
ring_theory/ideal/local_ring.lean 5.42
ring_theory/ideal/operations.lean 37.24
ring_theory/ideal/over.lean 19.65
ring_theory/ideal/prod.lean 9.09
ring_theory/int/basic.lean 8.81
ring_theory/integral_closure.lean 26.55
ring_theory/integral_domain.lean 9.20
ring_theory/integrally_closed.lean 9.49
ring_theory/jacobson.lean 54.97
ring_theory/jacobson_ideal.lean 8.84
ring_theory/laurent_series.lean 13.73
ring_theory/localization.lean 55.56
ring_theory/matrix_algebra.lean 26.25
ring_theory/multiplicity.lean 11.64
ring_theory/mv_polynomial/basic.lean 5.63
ring_theory/nakayama.lean 5.59
ring_theory/nilpotent.lean 3.31
ring_theory/noetherian.lean 22.77
ring_theory/non_zero_divisors.lean 2.65
ring_theory/norm.lean 18.44
ring_theory/nullstellensatz.lean 16.66
ring_theory/perfection.lean 35.08
ring_theory/polynomial/basic.lean 65.20
ring_theory/polynomial/bernstein.lean 36.17
ring_theory/polynomial/chebyshev.lean 10.75
ring_theory/polynomial/content.lean 15.39
ring_theory/polynomial/cyclotomic.lean 23.05
ring_theory/polynomial/default.lean 3.44
ring_theory/polynomial/dickson.lean 13.53
ring_theory/polynomial/gauss_lemma.lean 14.44
ring_theory/polynomial/homogeneous.lean 10.60
ring_theory/polynomial/pochhammer.lean 6.34
ring_theory/polynomial/rational_root.lean 7.12
ring_theory/polynomial/scale_roots.lean 11.50
ring_theory/polynomial/symmetric.lean 8.93
ring_theory/polynomial/tower.lean 3.17
ring_theory/polynomial/vieta.lean 5.39
ring_theory/polynomial_algebra.lean 27.98
ring_theory/power_basis.lean 31.10
ring_theory/power_series/basic.lean 99.58
ring_theory/power_series/well_known.lean 24.58
ring_theory/prime.lean 2.82
ring_theory/principal_ideal_domain.lean 12.84
ring_theory/ring_invo.lean 1.11
ring_theory/roots_of_unity.lean 25.05
ring_theory/simple_module.lean 4.68
ring_theory/subring.lean 9.98
ring_theory/subsemiring.lean 7.20
ring_theory/tensor_product.lean 107.52
ring_theory/trace.lean 31.08
ring_theory/unique_factorization_domain.lean 42.07
ring_theory/valuation/basic.lean 11.43
ring_theory/valuation/integers.lean 3.33
ring_theory/valuation/integral.lean 4.83
ring_theory/witt_vector/basic.lean 62.69
ring_theory/witt_vector/compare.lean 10.00
ring_theory/witt_vector/defs.lean 26.14
ring_theory/witt_vector/frobenius.lean 17.15
ring_theory/witt_vector/identities.lean 5.35
ring_theory/witt_vector/init_tail.lean 19.39
ring_theory/witt_vector/is_poly.lean 36.58
ring_theory/witt_vector/mul_p.lean 9.47
ring_theory/witt_vector/structure_polynomial.lean 34.49
ring_theory/witt_vector/teichmuller.lean 7.79
ring_theory/witt_vector/truncated.lean 15.75
ring_theory/witt_vector/verschiebung.lean 7.91
ring_theory/witt_vector/witt_polynomial.lean 10.61
set_theory/cardinal.lean 9.23
set_theory/cardinal_ordinal.lean 12.65
set_theory/cofinality.lean 10.57
set_theory/continuum.lean 2.61
set_theory/fincard.lean 1.99
set_theory/game.lean 12.89
set_theory/game/domineering.lean 4.09
set_theory/game/impartial.lean 3.18
set_theory/game/nim.lean 7.90
set_theory/game/short.lean 3.32
set_theory/game/state.lean 3.05
set_theory/game/winner.lean 2.21
set_theory/lists.lean 4.20
set_theory/ordinal.lean 10.39
set_theory/ordinal_arithmetic.lean 15.81
set_theory/ordinal_notation.lean 16.87
set_theory/pgame.lean 9.65
set_theory/schroeder_bernstein.lean 2.16
set_theory/surreal/basic.lean 3.19
set_theory/surreal/dyadic.lean 7.80
set_theory/zfc.lean 3.63
system/random/basic.lean 2.71
tactic/abel.lean 6.17
tactic/algebra.lean 0.43
tactic/alias.lean 0.54
tactic/apply.lean 0.49
tactic/apply_fun.lean 1.69
tactic/auto_cases.lean 0.52
tactic/basic.lean 0.56
tactic/binder_matching.lean 0.45
tactic/cache.lean 0.37
tactic/cancel_denoms.lean 3.57
tactic/chain.lean 0.70
tactic/choose.lean 0.53
tactic/clear.lean 0.46
tactic/congr.lean 0.57
tactic/converter/apply_congr.lean 0.47
tactic/converter/binders.lean 1.92
tactic/converter/interactive.lean 0.53
tactic/converter/old_conv.lean 0.49
tactic/core.lean 1.66
tactic/dec_trivial.lean 0.47
tactic/default.lean 2.13
tactic/delta_instance.lean 0.46
tactic/dependencies.lean 0.59
tactic/derive_fintype.lean 2.13
tactic/derive_inhabited.lean 0.38
tactic/doc_commands.lean 0.47
tactic/elementwise.lean 1.89
tactic/elide.lean 0.47
tactic/equiv_rw.lean 2.06
tactic/explode.lean 0.77
tactic/explode_widget.lean 0.63
tactic/ext.lean 0.76
tactic/field_simp.lean 1.94
tactic/fin_cases.lean 2.01
tactic/find.lean 0.50
tactic/find_unused.lean 0.46
tactic/finish.lean 0.82
tactic/fix_reflect_string.lean 0.34
tactic/fresh_names.lean 0.45
tactic/generalize_proofs.lean 0.34
tactic/generalizes.lean 0.54
tactic/group.lean 2.10
tactic/has_variable_names.lean 0.63
tactic/hint.lean 0.55
tactic/induction.lean 1.24
tactic/interactive.lean 1.21
tactic/interactive_expr.lean 0.61
tactic/interval_cases.lean 2.37
tactic/itauto.lean 0.97
tactic/lean_core_docs.lean 0.43
tactic/lift.lean 0.59
tactic/linarith/datatypes.lean 2.44
tactic/linarith/default.lean 1.89
tactic/linarith/elimination.lean 2.39
tactic/linarith/frontend.lean 2.23
tactic/linarith/lemmas.lean 4.84
tactic/linarith/parsing.lean 2.27
tactic/linarith/preprocessing.lean 4.16
tactic/linarith/verification.lean 2.00
tactic/lint/basic.lean 0.48
tactic/lint/default.lean 0.49
tactic/lint/frontend.lean 0.60
tactic/lint/misc.lean 3.01
tactic/lint/simp.lean 0.60
tactic/lint/type_classes.lean 0.71
tactic/local_cache.lean 2.46
tactic/localized.lean 0.48
tactic/mk_iff_of_inductive_prop.lean 0.61
tactic/monotonicity/basic.lean 0.92
tactic/monotonicity/default.lean 1.41
tactic/monotonicity/interactive.lean 2.41
tactic/monotonicity/lemmas.lean 1.70
tactic/noncomm_ring.lean 1.86
tactic/norm_cast.lean 1.21
tactic/norm_fin.lean 4.53
tactic/norm_num.lean 7.08
tactic/norm_swap.lean 2.04
tactic/nth_rewrite/basic.lean 0.39
tactic/nth_rewrite/congr.lean 0.49
tactic/nth_rewrite/default.lean 0.49
tactic/obviously.lean 0.49
tactic/omega/clause.lean 1.95
tactic/omega/coeffs.lean 4.03
tactic/omega/default.lean 1.89
tactic/omega/eq_elim.lean 5.48
tactic/omega/find_ees.lean 2.09
tactic/omega/find_scalars.lean 1.92
tactic/omega/int/dnf.lean 3.18
tactic/omega/int/form.lean 2.06
tactic/omega/int/main.lean 2.52
tactic/omega/int/preterm.lean 2.38
tactic/omega/lin_comb.lean 2.11
tactic/omega/main.lean 2.10
tactic/omega/misc.lean 0.49
tactic/omega/nat/dnf.lean 3.20
tactic/omega/nat/form.lean 2.22
tactic/omega/nat/main.lean 2.64
tactic/omega/nat/neg_elim.lean 2.55
tactic/omega/nat/preterm.lean 2.67
tactic/omega/nat/sub_elim.lean 2.72
tactic/omega/prove_unsats.lean 1.93
tactic/omega/term.lean 2.38
tactic/pi_instances.lean 0.61
tactic/pretty_cases.lean 0.44
tactic/protected.lean 0.43
tactic/push_neg.lean 0.60
tactic/rcases.lean 1.00
tactic/reassoc_axiom.lean 1.50
tactic/rename_var.lean 0.49
tactic/replacer.lean 0.52
tactic/reserved_notation.lean 0.29
tactic/restate_axiom.lean 0.36
tactic/rewrite.lean 0.61
tactic/rewrite_all/basic.lean 0.50
tactic/rewrite_search/default.lean 1.53
tactic/rewrite_search/discovery.lean 0.48
tactic/rewrite_search/explain.lean 0.88
tactic/rewrite_search/frontend.lean 1.64
tactic/rewrite_search/search.lean 1.74
tactic/rewrite_search/types.lean 0.46
tactic/ring.lean 11.17
tactic/ring2.lean 9.35
tactic/ring_exp.lean 10.47
tactic/scc.lean 0.66
tactic/show_term.lean 0.41
tactic/simp_command.lean 0.46
tactic/simp_result.lean 0.43
tactic/simp_rw.lean 0.43
tactic/simpa.lean 0.35
tactic/simps.lean 1.40
tactic/slice.lean 1.34
tactic/slim_check.lean 2.22
tactic/solve_by_elim.lean 0.58
tactic/split_ifs.lean 0.57
tactic/squeeze.lean 0.79
tactic/subtype_instance.lean 1.50
tactic/suggest.lean 0.85
tactic/tauto.lean 0.92
tactic/tfae.lean 1.72
tactic/tidy.lean 0.55
tactic/transfer.lean 0.55
tactic/transform_decl.lean 0.48
tactic/transport.lean 1.94
tactic/trunc_cases.lean 0.51
tactic/unfold_cases.lean 0.77
tactic/unify_equations.lean 0.77
tactic/where.lean 0.52
tactic/with_local_reducibility.lean 0.44
tactic/wlog.lean 1.77
tactic/zify.lean 1.61
testing/slim_check/functions.lean 6.06
testing/slim_check/gen.lean 3.01
testing/slim_check/sampleable.lean 9.93
testing/slim_check/testable.lean 3.17
topology/G_delta.lean 4.20
topology/alexandroff.lean 5.35
topology/algebra/affine.lean 5.60
topology/algebra/algebra.lean 4.25
topology/algebra/field.lean 3.83
topology/algebra/floor_ring.lean 7.42
topology/algebra/group.lean 10.94
topology/algebra/group_completion.lean 6.21
topology/algebra/group_with_zero.lean 3.17
topology/algebra/infinite_sum.lean 22.62
topology/algebra/localization.lean 4.67
topology/algebra/module.lean 59.70
topology/algebra/monoid.lean 5.96
topology/algebra/mul_action.lean 8.83
topology/algebra/multilinear.lean 5.66
topology/algebra/nonarchimedean/basic.lean 4.16
topology/algebra/open_subgroup.lean 6.17
topology/algebra/ordered/basic.lean 38.18
topology/algebra/ordered/extend_from.lean 3.67
topology/algebra/ordered/liminf_limsup.lean 3.29
topology/algebra/ordered/proj_Icc.lean 3.21
topology/algebra/polynomial.lean 7.62
topology/algebra/ring.lean 4.29
topology/algebra/uniform_field.lean 6.57
topology/algebra/uniform_group.lean 16.93
topology/algebra/uniform_ring.lean 6.65
topology/algebra/weak_dual_topology.lean 3.65
topology/bases.lean 5.99
topology/basic.lean 7.96
topology/category/CompHaus/default.lean 11.95
topology/category/CompHaus/projective.lean 5.10
topology/category/Compactum.lean 19.91
topology/category/Profinite/as_limit.lean 7.65
topology/category/Profinite/cofiltered_limit.lean 18.43
topology/category/Profinite/default.lean 17.82
topology/category/Profinite/projective.lean 5.04
topology/category/Top/adjunctions.lean 3.51
topology/category/Top/basic.lean 6.61
topology/category/Top/default.lean 3.07
topology/category/Top/epi_mono.lean 2.80
topology/category/Top/limits.lean 17.10
topology/category/Top/open_nhds.lean 4.53
topology/category/Top/opens.lean 5.11
topology/category/TopCommRing.lean 8.26
topology/category/UniformSpace.lean 5.42
topology/compact_open.lean 7.36
topology/compacts.lean 2.96
topology/connected.lean 9.24
topology/constructions.lean 15.12
topology/continuous_function/algebra.lean 25.37
topology/continuous_function/basic.lean 8.63
topology/continuous_function/bounded.lean 31.60
topology/continuous_function/compact.lean 28.45
topology/continuous_function/locally_constant.lean 11.94
topology/continuous_function/polynomial.lean 22.32
topology/continuous_function/stone_weierstrass.lean 35.77
topology/continuous_function/weierstrass.lean 6.87
topology/continuous_on.lean 17.84
topology/dense_embedding.lean 4.27
topology/discrete_quotient.lean 6.38
topology/extend_from.lean 3.05
topology/fiber_bundle.lean 26.46
topology/homeomorph.lean 4.39
topology/homotopy.lean 17.38
topology/instances/ennreal.lean 34.83
topology/instances/ereal.lean 14.82
topology/instances/nnreal.lean 7.19
topology/instances/real.lean 10.66
topology/instances/real_vector_space.lean 3.30
topology/list.lean 5.80
topology/local_extr.lean 2.86
topology/local_homeomorph.lean 10.76
topology/locally_constant/algebra.lean 5.64
topology/locally_constant/basic.lean 10.07
topology/maps.lean 3.95
topology/metric_space/algebra.lean 6.16
topology/metric_space/antilipschitz.lean 5.11
topology/metric_space/baire.lean 7.34
topology/metric_space/basic.lean 28.81
topology/metric_space/cau_seq_filter.lean 7.13
topology/metric_space/closeds.lean 8.48
topology/metric_space/completion.lean 6.87
topology/metric_space/contracting.lean 7.68
topology/metric_space/emetric_paracompact.lean 8.20
topology/metric_space/emetric_space.lean 27.50
topology/metric_space/gluing.lean 11.43
topology/metric_space/gromov_hausdorff.lean 38.96
topology/metric_space/gromov_hausdorff_realized.lean 20.69
topology/metric_space/hausdorff_dimension.lean 14.74
topology/metric_space/hausdorff_distance.lean 13.40
topology/metric_space/holder.lean 7.27
topology/metric_space/isometry.lean 5.24
topology/metric_space/kuratowski.lean 6.35
topology/metric_space/lipschitz.lean 6.64
topology/metric_space/metric_separated.lean 3.91
topology/metric_space/shrinking_lemma.lean 3.93
topology/omega_complete_partial_order.lean 5.58
topology/opens.lean 4.37
topology/order.lean 4.87
topology/paracompact.lean 4.60
topology/partition_of_unity.lean 7.82
topology/path_connected.lean 29.52
topology/semicontinuous.lean 11.07
topology/separation.lean 11.65
topology/sequences.lean 6.78
topology/sheaves/forget.lean 24.88
topology/sheaves/limits.lean 3.46
topology/sheaves/local_predicate.lean 21.00
topology/sheaves/presheaf.lean 7.68
topology/sheaves/presheaf_of_functions.lean 17.51
topology/sheaves/sheaf.lean 3.72
topology/sheaves/sheaf_condition/equalizer_products.lean 17.56
topology/sheaves/sheaf_condition/opens_le_cover.lean 6.48
topology/sheaves/sheaf_condition/pairwise_intersections.lean 50.20
topology/sheaves/sheaf_condition/unique_gluing.lean 12.36
topology/sheaves/sheaf_of_functions.lean 6.06
topology/sheaves/sheafify.lean 8.91
topology/sheaves/stalks.lean 20.40
topology/shrinking_lemma.lean 4.60
topology/stone_cech.lean 3.68
topology/subset_properties.lean 18.99
topology/tactic.lean 2.25
topology/uniform_space/absolute_value.lean 3.84
topology/uniform_space/abstract_completion.lean 2.96
topology/uniform_space/basic.lean 13.60
topology/uniform_space/cauchy.lean 6.61
topology/uniform_space/compact_separated.lean 5.85
topology/uniform_space/compare_reals.lean 4.97
topology/uniform_space/complete_separated.lean 2.67
topology/uniform_space/completion.lean 5.29
topology/uniform_space/pi.lean 2.77
topology/uniform_space/separation.lean 6.90
topology/uniform_space/uniform_convergence.lean 4.36
topology/uniform_space/uniform_embedding.lean 6.03
topology/unit_interval.lean 6.69
topology/urysohns_lemma.lean 7.75
topology/vector_bundle.lean 10.21