-
-
Save kckennylau/fd94d8c3a1cd2be9953deffd53657185 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| data/zmod/quadratic_reciprocity.lean 119 | |
| linear_algebra/basic.lean 87.1 | |
| data/rat.lean 78 | |
| data/padics/padic_numbers.lean 73 | |
| data/polynomial.lean 67.8 | |
| data/complex/basic.lean 66.8 | |
| data/set/basic.lean 64.4 | |
| group_theory/perm.lean 63.3 | |
| analysis/normed_space.lean 60.4 | |
| data/seq/wseq.lean 57.9 | |
| data/real/basic.lean 57.9 | |
| data/real/ennreal.lean 55.7 | |
| set_theory/ordinal_notation.lean 54.9 | |
| data/padics/padic_norm.lean 53.8 | |
| data/multiset.lean 53.4 | |
| data/num/lemmas.lean 50.7 | |
| analysis/topology/infinite_sum.lean 50.4 | |
| order/conditionally_complete_lattice.lean 49.2 | |
| computability/partrec_code.lean 47.6 | |
| number_theory/pell.lean 45.8 | |
| data/real/nnreal.lean 44.5 | |
| analysis/topology/continuity.lean 42.8 | |
| data/list/basic.lean 41 | |
| data/fintype.lean 39.7 | |
| linear_algebra/multivariate_polynomial.lean 39.1 | |
| analysis/measure_theory/outer_measure.lean 38.9 | |
| analysis/topology/topological_structures.lean 38.5 | |
| data/int/basic.lean 38.2 | |
| data/padics/hensel.lean 36.5 | |
| set_theory/cardinal.lean 33.6 | |
| set_theory/cofinality.lean 32.6 | |
| set_theory/ordinal.lean 32.5 | |
| data/padics/padic_integers.lean 32.4 | |
| computability/turing_machine.lean 31.6 | |
| group_theory/free_group.lean 31.5 | |
| algebra/module.lean 30.7 | |
| analysis/measure_theory/lebesgue_measure.lean 30.1 | |
| number_theory/dioph.lean 27.9 | |
| analysis/metric_space.lean 27.6 | |
| data/real/cau_seq.lean 27.1 | |
| computability/primrec.lean 27 | |
| data/holor.lean 26.9 | |
| linear_algebra/tensor_product.lean 25.5 | |
| computability/partrec.lean 25.2 | |
| analysis/measure_theory/measure_space.lean 23.3 | |
| ring_theory/associated.lean 22.5 | |
| data/set/lattice.lean 22.2 | |
| data/set/finite.lean 21.8 | |
| order/filter.lean 21 | |
| data/seq/computation.lean 20.4 | |
| category_theory/whiskering.lean 20.4 | |
| analysis/probability_mass_function.lean 20.4 | |
| analysis/real.lean 19.9 | |
| data/int/gcd.lean 19.6 | |
| data/hash_map.lean 19.6 | |
| data/list/perm.lean 19.3 | |
| algebra/big_operators.lean 19.3 | |
| category_theory/yoneda.lean 19.1 | |
| analysis/ennreal.lean 18.7 | |
| ring_theory/localization.lean 18.3 | |
| data/finset.lean 17.6 | |
| order/lattice.lean 17.2 | |
| data/seq/seq.lean 17.2 | |
| ring_theory/matrix.lean 16.3 | |
| order/complete_lattice.lean 16.3 | |
| data/real/cau_seq_filter.lean 16.2 | |
| analysis/measure_theory/measurable_space.lean 16.2 | |
| tests/finish2.lean 15.4 | |
| data/zmod/basic.lean 15 | |
| linear_algebra/submodule.lean 14.8 | |
| computability/halting.lean 14.7 | |
| analysis/topology/uniform_space.lean 14.5 | |
| linear_algebra/linear_map_module.lean 14.4 | |
| group_theory/order_of_element.lean 14.3 | |
| tactic/linarith.lean 13.9 | |
| data/analysis/topology.lean 13.9 | |
| tactic/ring2.lean 13.8 | |
| ring_theory/unique_factorization_domain.lean 13.3 | |
| field_theory/finite.lean 13 | |
| order/liminf_limsup.lean 12.2 | |
| data/equiv/list.lean 11.7 | |
| analysis/limits.lean 11.5 | |
| data/real/cau_seq_completion.lean 10.3 | |
| data/analysis/filter.lean 10 | |
| tactic/norm_num.lean 9.95 | |
| data/nat/basic.lean 9.79 | |
| data/finsupp.lean 9.7 | |
| analysis/topology/topological_space.lean 9.53 | |
| data/seq/parallel.lean 9.45 | |
| analysis/bounded_linear_maps.lean 9 | |
| group_theory/subgroup.lean 8.83 | |
| tactic/ring.lean 8.28 | |
| data/vector2.lean 8.13 | |
| category_theory/natural_isomorphism.lean 8.09 | |
| data/set/countable.lean 7.9 | |
| set_theory/zfc.lean 7.86 | |
| algebra/ordered_group.lean 7.35 | |
| data/set/enumerate.lean 7.34 | |
| data/set/intervals.lean 7.22 | |
| algebra/group_power.lean 7.07 | |
| tactic/abel.lean 7.04 | |
| data/array/lemmas.lean 7.02 | |
| data/nat/pairing.lean 6.98 | |
| analysis/topology/continuous_map.lean 6.96 | |
| category/traversable/instances.lean 6.94 | |
| data/equiv/basic.lean 6.66 | |
| group_theory/coset.lean 6.53 | |
| ring_theory/ideals.lean 6.21 | |
| algebra/pi_instances.lean 5.95 | |
| category_theory/products.lean 5.92 | |
| data/list/sort.lean 5.91 | |
| tests/tactics.lean 5.78 | |
| order/bounded_lattice.lean 5.69 | |
| algebra/ring.lean 5.64 | |
| tests/ring.lean 5.61 | |
| set_theory/lists.lean 5.57 | |
| algebra/ordered_ring.lean 5.57 | |
| data/pfun.lean 5.48 | |
| algebra/archimedean.lean 5.45 | |
| data/nat/prime.lean 5.43 | |
| ring_theory/noetherian.lean 5.37 | |
| tests/norm_num.lean 5.22 | |
| linear_algebra/subtype_module.lean 5.22 | |
| data/nat/totient.lean 5.05 | |
| data/semiquot.lean 4.98 | |
| linear_algebra/quotient_module.lean 4.9 | |
| category_theory/isomorphism.lean 4.75 | |
| order/boolean_algebra.lean 4.39 | |
| data/nat/sqrt.lean 4.36 | |
| data/nat/modeq.lean 4.25 | |
| algebra/order_functions.lean 4.23 | |
| tests/linarith.lean 4.22 | |
| tests/examples.lean 4.03 | |
| data/set/disjointed.lean 3.91 | |
| tests/finish3.lean 3.82 | |
| data/equiv/encodable.lean 3.76 | |
| data/buffer/basic.lean 3.61 | |
| data/int/modeq.lean 3.59 | |
| order/order_iso.lean 3.51 | |
| algebra/field_power.lean 3.32 | |
| algebra/group.lean 3.23 | |
| linear_algebra/prod_module.lean 3.19 | |
| data/equiv/denumerable.lean 3.18 | |
| algebra/gcd_domain.lean 3.18 | |
| analysis/measure_theory/borel_space.lean 3.16 | |
| order/zorn.lean 3.06 | |
| group_theory/submonoid.lean 2.85 | |
| data/option.lean 2.74 | |
| category/traversable/equiv.lean 2.67 | |
| data/bool.lean 2.64 | |
| data/nat/cast.lean 2.5 | |
| analysis/nnreal.lean 2.39 | |
| algebra/ordered_field.lean 2.39 | |
| data/fp/basic.lean 2.34 | |
| category_theory/examples/topological_spaces.lean 2.34 | |
| group_theory/abelianization.lean 2.28 | |
| ring_theory/principal_ideal_domain.lean 2.26 | |
| group_theory/free_abelian_group.lean 2.25 | |
| group_theory/group_action.lean 2.23 | |
| analysis/complex.lean 2.1 | |
| category_theory/natural_transformation.lean 2.05 | |
| tests/finish1.lean 2.04 | |
| logic/basic.lean 2.03 | |
| category_theory/embedding.lean 2.03 | |
| order/galois_connection.lean 1.92 | |
| data/nat/gcd.lean 1.81 | |
| order/basic.lean 1.8 | |
| category_theory/types.lean 1.78 | |
| category/applicative.lean 1.73 | |
| logic/schroeder_bernstein.lean 1.65 | |
| group_theory/quotient_group.lean 1.6 | |
| data/lazy_list2.lean 1.46 | |
| data/nat/binomial.lean 1.45 | |
| ring_theory/subring.lean 1.4 | |
| order/bounds.lean 1.38 | |
| category/traversable/lemmas.lean 1.38 | |
| analysis/polynomial.lean 1.36 | |
| data/string.lean 1.35 | |
| category_theory/category.lean 1.34 | |
| algebra/euclidean_domain.lean 1.3 | |
| data/nat/choose.lean 1.28 | |
| logic/relation.lean 1.18 | |
| field_theory/subfield.lean 1.16 | |
| data/real/irrational.lean 1.13 | |
| category/basic.lean 1.13 | |
| algebra/field.lean 1.11 | |
| tactic/tauto.lean 1.08 | |
| order/complete_boolean_algebra.lean 1.05 | |
| logic/embedding.lean 1.05 | |
| data/nat/dist.lean 1.03 | |
| category_theory/opposites.lean 0.997 | |
| category_theory/full_subcategory.lean 0.876 | |
| tactic/converter/binders.lean 0.864 | |
| linear_algebra/dimension.lean 0.864 | |
| tactic/basic.lean 0.858 | |
| data/num/basic.lean 0.845 | |
| category_theory/examples/rings.lean 0.787 | |
| tactic/interactive.lean 0.778 | |
| category/traversable/derive.lean 0.757 | |
| tactic/wlog.lean 0.703 | |
| category_theory/functor_category.lean 0.676 | |
| category_theory/functor.lean 0.645 | |
| order/fixed_points.lean 0.627 | |
| data/erased.lean 0.623 | |
| data/prod.lean 0.587 | |
| category_theory/examples/monoids.lean 0.569 | |
| data/fin.lean 0.544 | |
| tactic/finish.lean 0.458 | |
| logic/function.lean 0.434 | |
| data/set/function.lean 0.413 | |
| tactic/rcases.lean 0.405 | |
| category/functor.lean 0.379 | |
| tactic/rewrite.lean 0.365 | |
| tests/tidy.lean 0.357 | |
| tactic/ext.lean 0.356 | |
| data/equiv/nat.lean 0.35 | |
| tactic/scc.lean 0.331 | |
| algebra/char_zero.lean 0.325 | |
| tactic/converter/old_conv.lean 0.316 | |
| category_theory/groupoid.lean 0.303 | |
| data/dlist/instances.lean 0.297 | |
| data/num/bitwise.lean 0.269 | |
| data/quot.lean 0.257 | |
| tactic/generalize_proofs.lean 0.248 | |
| tactic/replacer.lean 0.242 | |
| tactic/alias.lean 0.24 | |
| tactic/squeeze.lean 0.203 | |
| algebra/order.lean 0.194 | |
| tactic/mk_iff_of_inductive_prop.lean 0.187 | |
| category/traversable/basic.lean 0.185 | |
| data/sum.lean 0.178 | |
| category_theory/examples/measurable_space.lean 0.159 | |
| tactic/split_ifs.lean 0.145 | |
| data/sigma/basic.lean 0.139 | |
| tactic/tidy.lean 0.138 | |
| tactic/find.lean 0.127 | |
| tactic/chain.lean 0.118 | |
| tactic/tfae.lean 0.109 | |
| tactic/auto_cases.lean 0.0891 | |
| tactic/explode.lean 0.0874 | |
| tactic/subtype_instance.lean 0.0866 | |
| data/subtype.lean 0.0856 | |
| tactic/pi_instances.lean 0.0683 | |
| tactic/converter/interactive.lean 0.062200000000000005 | |
| tests/split_ifs.lean 0.057 | |
| meta/rb_map.lean 0.0451 | |
| tactic/restate_axiom.lean 0.0446 | |
| tests/mk_iff_of_inductive.lean 0.043 | |
| tactic/algebra.lean 0.039799999999999995 | |
| data/pnat.lean 0.036899999999999995 | |
| tactic/cache.lean 0.0334 | |
| tests/replacer.lean 0.030100000000000002 | |
| logic/relator.lean 0.0255 | |
| tests/restate_axiom.lean 0.0156 | |
| core/data/list.lean 0.015300000000000001 | |
| data/char.lean 0.010199999999999999 | |
| data/dlist/basic.lean 0.00923 | |
| tactic/default.lean 0 | |
| pending/default.lean 0 | |
| order/default.lean 0 | |
| linear_algebra/default.lean 0 | |
| data/stream/basic.lean 0 | |
| data/sigma/default.lean 0 | |
| data/set/default.lean 0 | |
| data/padics/default.lean 0 | |
| data/list/default.lean 0 | |
| core/default.lean 0 | |
| category/traversable/default.lean 0 | |
| algebra/default.lean 0 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment