Skip to content

Instantly share code, notes, and snippets.

@kckennylau
Created May 13, 2020 15:40
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kckennylau/cc14edf26842ac3ecd8f54bb26858f4b to your computer and use it in GitHub Desktop.
Save kckennylau/cc14edf26842ac3ecd8f54bb26858f4b to your computer and use it in GitHub Desktop.
0.04807339449541284 src/topology/category/Top/adjunctions.lean
0.020389546351084812 src/category_theory/elements.lean
0.015910462500685795 src/category_theory/limits/shapes/binary_products.lean
0.015718349928876246 src/analysis/normed_space/hahn_banach.lean
0.014868532998419965 src/analysis/special_functions/pow.lean
0.014746689923095219 src/category_theory/limits/over.lean
0.013920285544318858 src/analysis/complex/basic.lean
0.013886572143452876 src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean
0.013393418570530287 src/measure_theory/probability_mass_function.lean
0.013363333985521423 src/algebra/homology/homology.lean
0.012804698972099854 src/category_theory/graded_object.lean
0.012802926383173296 src/topology/sheaves/presheaf.lean
0.012098366541015976 src/algebra/category/Module/monoidal.lean
0.011772905842098594 src/category_theory/limits/shapes/wide_pullbacks.lean
0.011354838709677418 src/category_theory/adjunction/limits.lean
0.011281224818694601 src/category_theory/pempty.lean
0.010924593658406609 src/topology/metric_space/cau_seq_filter.lean
0.010811648079306072 src/category_theory/currying.lean
0.010690172543135784 src/data/padics/padic_integers.lean
0.010124164278892072 src/algebraic_geometry/stalks.lean
0.010049800349948405 src/category_theory/comma.lean
0.009878067603025158 src/data/complex/basic.lean
0.009786665857433314 src/analysis/special_functions/trigonometric.lean
0.009620741375616026 src/order/complete_boolean_algebra.lean
0.009548538403551386 src/number_theory/sum_four_squares.lean
0.009487750556792874 src/category_theory/monoidal/of_has_finite_products.lean
0.009478071765132294 src/algebra/category/Group/biproducts.lean
0.009176182707993474 src/data/real/cardinality.lean
0.008574166540575983 src/measure_theory/outer_measure.lean
0.008479349186483104 src/topology/category/UniformSpace.lean
0.00834002594674739 src/topology/metric_space/hausdorff_distance.lean
0.008241060083499728 src/data/matrix/notation.lean
0.007862955032119914 src/linear_algebra/quadratic_form.lean
0.00776476175399715 src/data/zsqrtd/gaussian_int.lean
0.007735176782288272 src/data/dfinsupp.lean
0.007711767586094337 src/measure_theory/lebesgue_measure.lean
0.007525476874836686 src/data/matrix/basic.lean
0.007462686567164179 src/algebra/category/Group/adjunctions.lean
0.0074252320385012035 test/transport/basic.lean
0.0072732225551620806 src/category_theory/differential_object.lean
0.007196870925684484 src/algebra/category/Group/zero.lean
0.0071204516938519445 src/data/int/parity.lean
0.007100914925576949 src/analysis/normed_space/real_inner_product.lean
0.007078093009651945 src/ring_theory/principal_ideal_domain.lean
0.006873614190687362 src/topology/sheaves/presheaf_of_functions.lean
0.006764667620658254 src/analysis/calculus/specific_functions.lean
0.006554242002781641 src/algebra/category/Module/basic.lean
0.006538796861377506 archive/sensitivity.lean
0.006500908894845488 src/data/padics/padic_numbers.lean
0.006456738408204536 src/category_theory/monad/algebra.lean
0.0064415956684449405 src/data/real/pi.lean
0.0064240790655885 src/category_theory/adjunction/fully_faithful.lean
0.006246773360867321 src/analysis/normed_space/bounded_linear_maps.lean
0.006204606764888981 src/category_theory/limits/functor_category.lean
0.006203566121842496 src/topology/category/TopCommRing.lean
0.006050637372965987 src/linear_algebra/finsupp.lean
0.0059693243056515135 src/algebra/category/CommRing/basic.lean
0.005966666666666666 src/number_theory/bernoulli.lean
0.0058980582524271845 src/ring_theory/adjoin_root.lean
0.005652173913043478 src/field_theory/splitting_field.lean
0.005608465608465609 src/category_theory/category/Groupoid.lean
0.005602653888684113 src/category_theory/limits/shapes/constructions/equalizers.lean
0.005578443380469881 src/algebra/category/Group/basic.lean
0.005565749235474007 src/analysis/calculus/iterated_deriv.lean
0.005547376169944263 src/analysis/analytic/basic.lean
0.005468130872863126 src/linear_algebra/determinant.lean
0.005458799064205874 src/topology/category/Top/opens.lean
0.005389848246991104 src/data/matrix/pequiv.lean
0.005367590943780209 src/category_theory/limits/shapes/constructions/pullbacks.lean
0.005356943566087571 src/ring_theory/localization.lean
0.005355371900826446 src/algebra/classical_lie_algebras.lean
0.005267629566694987 src/category_theory/const.lean
0.005211442786069652 src/data/pnat/intervals.lean
0.005145709336031972 src/data/mv_polynomial.lean
0.0050933786078098476 src/topology/category/Top/open_nhds.lean
0.005067755708186375 src/analysis/normed_space/mazur_ulam.lean
0.005034568338946995 src/analysis/normed_space/multilinear.lean
0.004974455498789997 src/category_theory/limits/connected.lean
0.004965874323370205 src/measure_theory/giry_monad.lean
0.004944682772634906 src/field_theory/minimal_polynomial.lean
0.004912451361867704 src/topology/algebra/polynomial.lean
0.004842360549717058 src/algebra/category/Group/Z_Module_equivalence.lean
0.004791558553883411 src/category_theory/monad/adjunction.lean
0.004711848291162644 src/category_theory/limits/shapes/images.lean
0.004705882352941177 src/category_theory/yoneda.lean
0.004704 src/category_theory/discrete_category.lean
0.004672771343926744 src/field_theory/finite.lean
0.0046239087973851 src/number_theory/quadratic_reciprocity.lean
0.004614691978689878 src/category_theory/limits/cones.lean
0.004605497289036823 src/data/complex/exponential.lean
0.0045692527367920035 src/analysis/convex/specific_functions.lean
0.0045674368619022035 src/ring_theory/euclidean_domain.lean
0.004534925160370634 src/analysis/calculus/extend_deriv.lean
0.00445883986034577 src/data/monoid_algebra.lean
0.004428930675974928 src/data/polynomial.lean
0.004411392405063291 src/algebra/category/CommRing/adjunctions.lean
0.004380396140172676 src/topology/algebra/infinite_sum.lean
0.004372167422020795 src/linear_algebra/matrix.lean
0.004311388848520079 src/analysis/normed_space/basic.lean
0.004300937219155219 src/algebra/category/Mon/basic.lean
0.004300254452926209 src/number_theory/sum_two_squares.lean
0.004271333998367643 src/analysis/normed_space/banach.lean
0.004265194756319388 src/geometry/manifold/basic_smooth_bundle.lean
0.004219409282700422 src/category_theory/products/basic.lean
0.004215736473800989 src/analysis/special_functions/exp_log.lean
0.004152527237006608 src/data/pequiv.lean
0.0041308621794163775 src/data/real/ennreal.lean
0.004044610715041998 src/geometry/manifold/real_instances.lean
0.003960248075917209 src/linear_algebra/basis.lean
0.003934233705226072 src/linear_algebra/linear_action.lean
0.003923809523809524 src/ring_theory/integral_domain.lean
0.003914823914823915 src/analysis/complex/polynomial.lean
0.00390224674812771 src/category_theory/limits/shapes/pullbacks.lean
0.0038775268944319656 src/data/analysis/topology.lean
0.0037899543378995433 src/category_theory/hom_functor.lean
0.003769359955215525 src/category_theory/limits/types.lean
0.0037638776062821557 src/data/nat/parity.lean
0.0036509162395562734 src/ring_theory/fractional_ideal.lean
0.0036280765724703737 src/control/traversable/instances.lean
0.003605769230769231 src/analysis/calculus/deriv.lean
0.0035960029044638845 src/ring_theory/power_series.lean
0.0035825590539713976 src/combinatorics/composition.lean
0.003580320094842916 src/order/filter/partial.lean
0.0035531552018192155 src/linear_algebra/tensor_product.lean
0.0034820910403119 src/geometry/manifold/mfderiv.lean
0.003428851334802841 src/group_theory/perm/sign.lean
0.0034249067588465387 src/set_theory/cofinality.lean
0.003414531117994931 src/analysis/analytic/composition.lean
0.003385004745333755 src/category_theory/sums/associator.lean
0.0033669047897880314 src/data/padics/padic_norm.lean
0.0033364872267317366 src/linear_algebra/basic.lean
0.0033217121828394342 src/category_theory/monad/limits.lean
0.003299161230195713 test/apply.lean
0.003281667557455906 src/data/buffer/basic.lean
0.003245614035087719 src/category_theory/products/associator.lean
0.0032400932400932403 src/topology/metric_space/completion.lean
0.0032001958589815333 src/measure_theory/integration.lean
0.0031746031746031746 src/category_theory/single_obj.lean
0.003168095415579575 src/data/padics/hensel.lean
0.0031590156176053005 src/algebraic_geometry/presheafed_space.lean
0.003150942252923711 src/linear_algebra/multilinear.lean
0.0031457589898435355 src/data/finmap.lean
0.0031064923455134653 src/data/fin_enum.lean
0.0030566534914361 src/category_theory/core.lean
0.003054982817869416 src/analysis/normed_space/operator_norm.lean
0.003046661243806848 src/data/fintype/card.lean
0.003029315960912052 src/group_theory/coset.lean
0.003025287356321839 src/linear_algebra/dual.lean
0.0030118350174969527 src/topology/bounded_continuous_function.lean
0.003010719198525786 src/topology/instances/ennreal.lean
0.0029891947314456976 src/analysis/normed_space/finite_dimension.lean
0.0029821975280644067 src/algebra/lie_algebra.lean
0.002972071696540225 src/data/set/enumerate.lean
0.0029626449119793904 src/analysis/normed_space/riesz_lemma.lean
0.002958414736254535 src/data/holor.lean
0.0029482071713147406 src/data/real/ereal.lean
0.00293192654966014 src/ring_theory/unique_factorization_domain.lean
0.0029201502483945235 src/analysis/calculus/tangent_cone.lean
0.002913717041140864 src/algebra/floor.lean
0.0029040622299049265 src/ring_theory/multiplicity.lean
0.002903649105173521 src/set_theory/ordinal_notation.lean
0.00288 src/topology/sheaves/stalks.lean
0.0028704896907216495 src/category_theory/limits/shapes/products.lean
0.002867845019314058 src/algebra/category/Group/colimits.lean
0.002861982360843409 src/data/finsupp.lean
0.002845774814892888 src/measure_theory/measure_space.lean
0.0028404565967613486 src/algebra/category/Mon/colimits.lean
0.0028386291353327585 src/data/multiset.lean
0.0028301100366788933 src/topology/metric_space/gluing.lean
0.002826340326340326 src/algebra/quadratic_discriminant.lean
0.002822367260539778 src/topology/algebra/monoid.lean
0.0028145020923601083 src/category_theory/limits/shapes/equalizers.lean
0.0028142192128650023 src/data/real/cau_seq_completion.lean
0.0027926960257787323 src/topology/instances/nnreal.lean
0.0027858848500928626 src/topology/algebra/uniform_ring.lean
0.0027853525516166734 src/data/int/gcd.lean
0.002780528681343795 src/algebraic_geometry/prime_spectrum.lean
0.002763917212652406 archive/cubing_a_cube.lean
0.0027420343137254904 src/topology/algebra/uniform_group.lean
0.0027345293606259387 src/algebra/category/CommRing/colimits.lean
0.0026956972524624155 src/category_theory/whiskering.lean
0.0026930586413519155 src/analysis/calculus/local_extr.lean
0.002669340184222069 src/linear_algebra/bilinear_form.lean
0.0026635514018691587 src/category_theory/limits/limits.lean
0.002651021295089092 src/topology/uniform_space/separation.lean
0.002637423653525819 src/topology/metric_space/premetric_space.lean
0.0026321974148061106 src/category_theory/category/Rel.lean
0.00262840871755558 src/data/equiv/denumerable.lean
0.002621384982754046 src/ring_theory/ideals.lean
0.002617675312199808 src/topology/algebra/group_completion.lean
0.002607223476297968 src/category_theory/reflect_isomorphisms.lean
0.002605019500431689 src/topology/algebra/module.lean
0.0025805494790701123 src/topology/metric_space/gromov_hausdorff_realized.lean
0.002531364220092858 src/analysis/calculus/times_cont_diff.lean
0.0025198337740838686 src/algebra/category/Group/images.lean
0.0025197984161267097 src/data/set/countable.lean
0.0025175341454411223 src/category_theory/limits/shapes/strong_epi.lean
0.0025164628410159922 src/algebra/category/Group/limits.lean
0.002491684658925133 src/ring_theory/polynomial.lean
0.002486057918430424 src/topology/instances/real.lean
0.0024849543777907203 src/algebra/field_power.lean
0.0024499450874376954 src/data/analysis/filter.lean
0.00244987577280869 src/topology/algebra/group.lean
0.002447462839569452 src/data/indicator_function.lean
0.0024411508282476025 src/analysis/normed_space/point_reflection.lean
0.0024233352212962214 src/data/rat/basic.lean
0.0024226254002134473 src/data/set/disjointed.lean
0.0024157281012456722 src/data/real/nnreal.lean
0.002405328258801142 src/data/real/basic.lean
0.0023853211009174312 src/category_theory/adjunction/basic.lean
0.002359375412824645 src/analysis/convex/basic.lean
0.0023561090541905083 src/computability/partrec_code.lean
0.0023352247926669576 src/data/list/rotate.lean
0.0023284771510397213 src/data/list/sigma.lean
0.0022952230669918234 src/topology/metric_space/gromov_hausdorff.lean
0.002288732394366197 src/analysis/mean_inequalities.lean
0.002287470126322977 src/topology/uniform_space/absolute_value.lean
0.0022568287808127914 src/group_theory/order_of_element.lean
0.0022564687975646877 src/category_theory/eq_to_hom.lean
0.0022533022533022533 src/data/equiv/list.lean
0.002236149224949937 src/geometry/manifold/smooth_manifold_with_corners.lean
0.00222011385199241 src/control/equiv_functor/instances.lean
0.0022116903633491313 src/data/nat/multiplicity.lean
0.0021997621878715816 src/topology/compact_open.lean
0.0021981918099627726 src/measure_theory/ae_eq_fun.lean
0.0021857518615937465 src/data/zsqrtd/basic.lean
0.0021854771518297765 src/linear_algebra/nonsingular_inverse.lean
0.0021832770270270273 src/analysis/specific_limits.lean
0.002174809925148818 src/ring_theory/integral_closure.lean
0.002120882919362007 src/data/fintype/basic.lean
0.0021206096752816434 src/data/int/modeq.lean
0.0021155705996131527 src/data/real/cau_seq.lean
0.0021010101010101013 src/algebra/category/CommRing/limits.lean
0.002100896560952763 src/measure_theory/simple_func_dense.lean
0.0020946023708136724 src/set_theory/game/short.lean
0.002094076754323485 src/topology/metric_space/basic.lean
0.0020921237693389593 src/linear_algebra/special_linear_group.lean
0.0020761559383499547 src/category_theory/limits/shapes/terminal.lean
0.0020713551384076456 src/algebra/gcd_domain.lean
0.0020686484829911126 src/algebra/invertible.lean
0.0020411430401024574 src/analysis/calculus/fderiv.lean
0.002030680940293566 src/algebra/module.lean
0.002025 src/data/nat/pairing.lean
0.002007553170343868 src/category_theory/sums/basic.lean
0.001999182338511856 src/data/lazy_list2.lean
0.0019850912235904617 src/topology/topological_fiber_bundle.lean
0.0019774823597071382 src/set_theory/cardinal.lean
0.0019709804579384383 src/group_theory/sylow.lean
0.0019653488017096626 src/algebra/big_operators.lean
0.001958873404151642 src/data/vector2.lean
0.0019581845996940335 src/data/finsupp/pointwise.lean
0.0019546791212592977 src/ring_theory/noetherian.lean
0.001953965888392118 src/topology/algebra/open_subgroup.lean
0.0019399442781962647 src/algebra/pi_instances.lean
0.0019263122476446835 src/topology/algebra/multilinear.lean
0.001916354556803995 src/topology/metric_space/isometry.lean
0.0019113491001041202 src/computability/halting.lean
0.0018992456896551723 src/algebra/geom_sum.lean
0.0018863557458627474 src/order/lattice.lean
0.0018833207057040804 src/field_theory/mv_polynomial.lean
0.0018682858477347033 src/data/rel.lean
0.00184070796460177 src/data/rat/cast.lean
0.001830403309203723 src/group_theory/abelianization.lean
0.0018283731482717203 src/order/filter/filter_product.lean
0.0018157570783750513 src/group_theory/subgroup.lean
0.0017868675995694294 src/data/set/finite.lean
0.0017760003974266623 src/topology/metric_space/emetric_space.lean
0.0017746578853965374 src/algebra/direct_limit.lean
0.001768665149108298 src/data/finset.lean
0.0017680180180180182 src/category_theory/limits/concrete_category.lean
0.0017633928571428573 src/algebra/continued_fractions/translations.lean
0.0017527614260202395 src/topology/metric_space/baire.lean
0.0017467581998474447 src/data/equiv/nat.lean
0.0017380578605068401 src/ring_theory/algebra_operations.lean
0.0017357038123167157 src/topology/metric_space/antilipschitz.lean
0.0017309340188517567 src/analysis/calculus/darboux.lean
0.0017151548493576259 src/group_theory/free_group.lean
0.0017131474103585659 src/data/dlist/instances.lean
0.001707462686567164 src/algebra/associated.lean
0.0017036760589662252 src/category_theory/natural_isomorphism.lean
0.0016977724262492474 src/category_theory/limits/shapes/zero.lean
0.0016965797494073824 src/measure_theory/borel_space.lean
0.0016947723440134909 src/data/nat/totient.lean
0.0016806426608413784 src/computability/partrec.lean
0.0016678337258896174 src/linear_algebra/linear_pmap.lean
0.0016658156752616799 src/topology/uniform_space/basic.lean
0.001661906704746362 src/data/real/hyperreal.lean
0.0016570155902004456 src/data/list/min_max.lean
0.0016485424472265375 src/topology/subset_properties.lean
0.0016386641775565237 src/category_theory/opposites.lean
0.0016232514111418853 src/data/seq/seq.lean
0.0016158606463442585 src/control/bitraversable/instances.lean
0.0016060019928491882 src/linear_algebra/finite_dimensional.lean
0.0016005040957781979 src/set_theory/game/domineering.lean
0.0015818310357016612 src/data/list/sort.lean
0.0015735920492191198 src/topology/list.lean
0.0015588168200136871 src/topology/algebra/ordered.lean
0.0015558544476353192 src/data/seq/wseq.lean
0.0015534308845351918 src/data/int/basic.lean
0.001545673969550687 src/topology/metric_space/closeds.lean
0.0015260788142009004 src/data/num/lemmas.lean
0.0015093127809890816 src/data/rat/order.lean
0.0014993481095176009 src/group_theory/free_abelian_group.lean
0.0014985915492957747 src/data/array/lemmas.lean
0.001489295202375371 src/data/list/intervals.lean
0.0014585527915079814 src/algebra/pointwise.lean
0.0014554419284149014 src/category_theory/limits/shapes/regular_mono.lean
0.0014232799603348207 src/data/set/lattice.lean
0.0014109263657957245 src/algebra/direct_sum.lean
0.0014027935069837675 src/data/set/basic.lean
0.001389799396879507 src/analysis/convex/topology.lean
0.0013796441970228732 src/data/zmod/basic.lean
0.0013651705203768074 src/order/liminf_limsup.lean
0.0013623614264725522 src/measure_theory/set_integral.lean
0.0013513513513513512 src/analysis/calculus/inverse.lean
0.0013419483101391651 src/data/rat/floor.lean
0.0013271116735210377 src/topology/opens.lean
0.001320863309352518 src/data/list/bag_inter.lean
0.0013187311178247734 src/data/equiv/transfer_instance.lean
0.001298091961213638 src/data/nat/modeq.lean
0.0012710127101271014 src/algebra/char_p.lean
0.0012689393939393939 src/category_theory/monoidal/functor.lean
0.001266550755650662 src/group_theory/perm/cycles.lean
0.0012646370023419204 src/data/fin.lean
0.0012635474491144594 src/order/filter/pointwise.lean
0.0012519901577652337 archive/imo1988_q6.lean
0.001241429970617042 src/category_theory/functor_category.lean
0.001237354085603113 src/data/string/basic.lean
0.0012367270455965022 src/category_theory/monoidal/category.lean
0.0012341062079281975 src/category_theory/quotient.lean
0.0012339930151338766 src/measure_theory/decomposition.lean
0.0012180537715374053 src/data/pfun.lean
0.0012112259970457901 src/order/pilex.lean
0.0011879887767894453 src/topology/uniform_space/uniform_convergence.lean
0.0011839947523778287 src/topology/instances/complex.lean
0.0011583430540107967 src/number_theory/dioph.lean
0.0011578083690400218 src/data/list/alist.lean
0.0011516108201191076 src/data/hash_map.lean
0.0011500527714088148 src/ring_theory/algebra.lean
0.0011452513966480446 src/data/real/irrational.lean
0.0011439883309022714 src/control/traversable/equiv.lean
0.0011383924286345048 src/computability/primrec.lean
0.0011376465479808944 src/algebra/order_functions.lean
0.0011307420494699647 src/category_theory/limits/shapes/kernels.lean
0.0011043756967670012 src/measure_theory/l1_space.lean
0.00110435663627153 src/topology/local_homeomorph.lean
0.001099290780141844 test/finish4.lean
0.0010975829184909735 src/linear_algebra/dimension.lean
0.001072240339954541 src/topology/uniform_space/uniform_embedding.lean
0.001071817192600653 src/data/list/tfae.lean
0.0010708347189890258 src/category_theory/equivalence.lean
0.0010660276010247087 src/data/seq/parallel.lean
0.0010597826086956523 src/data/equiv/encodable.lean
0.001059090909090909 src/category_theory/groupoid.lean
0.0010497952899184658 src/data/set/intervals/basic.lean
0.0010485582324304083 src/ring_theory/free_comm_ring.lean
0.0010475 src/topology/algebra/ring.lean
0.0010443864229765013 src/category_theory/limits/lattice.lean
0.0010423961644130798 src/number_theory/pell.lean
0.0010340418026280977 src/measure_theory/measurable_space.lean
0.0010320641282565131 src/algebra/archimedean.lean
0.0010306290641018674 src/measure_theory/bochner_integration.lean
0.0010304054054054053 src/set_theory/lists.lean
0.001022256728778468 src/analysis/calculus/mean_value.lean
0.0010168769632114146 src/analysis/convex/cone.lean
0.0010153894970648897 src/data/nat/enat.lean
0.0010080387903534517 src/topology/separation.lean
0.001004917025199754 src/data/nat/fib.lean
0.0009926113889096202 src/data/pnat/xgcd.lean
0.0009871739443723878 src/data/nat/sqrt.lean
0.000982989999145226 src/category_theory/limits/shapes/biproducts.lean
0.0009819811230813234 src/tactic/ring2.lean
0.0009759914343367788 src/topology/continuous_on.lean
0.0009727294862429998 test/monotonicity.lean
0.0009705804254072318 src/computability/turing_machine.lean
0.0009699201964395335 src/category_theory/isomorphism_classes.lean
0.0009678534393363291 src/topology/constructions.lean
0.0009678329571106095 src/ring_theory/algebraic.lean
0.0009560648080572179 src/algebra/euclidean_domain.lean
0.0009507711810690894 src/data/support.lean
0.0009299333255351504 src/group_theory/group_action.lean
0.0009286675639300134 archive/examples/prop_encodable.lean
0.0009171563544187119 src/linear_algebra/sesquilinear_form.lean
0.0009160424469413234 src/linear_algebra/finsupp_vector_space.lean
0.0009035181236673774 src/data/equiv/fin.lean
0.0008992721296078892 src/data/nat/choose.lean
0.0008952080042127435 src/category_theory/types.lean
0.0008902050441952151 src/order/filter/basic.lean
0.0008865514650638617 src/data/nat/dist.lean
0.0008840244159124394 src/order/order_iso.lean
0.0008836667314041561 src/algebra/continued_fractions/convergents_equiv.lean
0.0008784188460770613 src/topology/uniform_space/cauchy.lean
0.0008613938919342208 src/data/nat/cast.lean
0.0008599644917887261 src/topology/basic.lean
0.0008594463036203225 src/tactic/abel.lean
0.0008536585365853659 src/data/pnat/factors.lean
0.0008494246629463183 src/data/nat/prime.lean
0.0008478853336025033 src/algebra/group_power.lean
0.0008438422323584653 src/data/semiquot.lean
0.0008291931985165489 src/order/filter/bases.lean
0.0008278145695364238 src/topology/maps.lean
0.0008208042302987255 src/algebra/ordered_ring.lean
0.000815189439396537 src/topology/metric_space/lipschitz.lean
0.0008118433619866284 src/set_theory/game/state.lean
0.0008104952263204891 src/topology/dense_embedding.lean
0.0008086021505376344 src/topology/uniform_space/completion.lean
0.0008012938322428876 src/geometry/manifold/manifold.lean
0.0007957724588125583 src/data/list/of_fn.lean
0.0007946892437944968 src/algebra/field.lean
0.0007894736842105263 src/data/list/antidiagonal.lean
0.0007793259883344134 src/category_theory/fully_faithful.lean
0.000765904879555281 src/category_theory/limits/shapes/finite_products.lean
0.0007653193586883205 src/data/list/basic.lean
0.0007647182065786717 src/algebra/group_with_zero.lean
0.0007568905602894273 src/data/nat/basic.lean
0.0007534775888717156 src/topology/metric_space/contracting.lean
0.0007478779536590961 src/tactic/ring.lean
0.0007436182019977803 docs/tutorial/Zmod37.lean
0.0007416413373860182 src/field_theory/subfield.lean
0.0007354817753648407 src/data/list/perm.lean
0.00072574410514109 src/data/list/func.lean
0.0007243631176588584 src/analysis/asymptotics.lean
0.0007203266258384369 src/algebra/continued_fractions/continuants_recurrence.lean
0.0006983893604223751 src/algebra/ring.lean
0.0006922650913789921 src/control/applicative.lean
0.0006910444716442269 src/set_theory/pgame.lean
0.0006894664842681258 src/control/traversable/lemmas.lean
0.0006880160120090068 src/ring_theory/adjoin.lean
0.0006796637453049544 src/order/conditionally_complete_lattice.lean
0.0006784090909090908 src/category_theory/connected.lean
0.0006677099634846114 src/algebra/group/conj.lean
0.0006654626285079189 src/group_theory/quotient_group.lean
0.0006565193471483587 src/data/list/zip.lean
0.0006560236114837671 src/algebra/group/with_one.lean
0.0006536388140161725 test/ext.lean
0.0006533018867924528 src/topology/sequences.lean
0.0006530612244897959 src/topology/category/Top/limits.lean
0.0006529229521961954 src/set_theory/ordinal.lean
0.0006512656672401082 src/algebra/free_monoid.lean
0.0006506991554755642 src/algebra/ordered_group.lean
0.0006485979925522207 src/group_theory/monoid_localization.lean
0.0006474820143884892 src/measure_theory/category/Meas.lean
0.0006411344079505515 src/data/list/range.lean
0.0006347325660121868 src/tactic/linarith.lean
0.0006328781512605043 src/category_theory/monoidal/functorial.lean
0.00062 src/set_theory/schroeder_bernstein.lean
0.000614495331258337 src/category_theory/limits/preserves.lean
0.0006105047748976807 src/category_theory/epi_mono.lean
0.0006101694915254237 src/measure_theory/indicator_function.lean
0.0006093544137022398 src/topology/bases.lean
0.0006032647267565649 src/category_theory/endomorphism.lean
0.0005919645585090132 src/ring_theory/ideal_operations.lean
0.0005895691609977325 src/data/equiv/functor.lean
0.0005865120172187015 src/field_theory/perfect_closure.lean
0.0005811320754716982 src/tactic/omega/coeffs.lean
0.000576220903696942 src/computability/reduce.lean
0.0005757290686735654 src/data/bool.lean
0.0005737373737373737 src/tactic/omega/nat/dnf.lean
0.0005731018615352438 src/topology/uniform_space/compare_reals.lean
0.0005549499554058072 src/group_theory/submonoid.lean
0.0005513895015438906 src/order/copy.lean
0.0005463966085727743 src/data/erased.lean
0.0005460944595821979 src/control/monad/cont.lean
0.0005399688265419728 src/algebra/group/prod.lean
0.0005392879713503265 src/algebra/ordered_field.lean
0.0005389696169088508 src/category_theory/category/default.lean
0.0005362478377103319 src/data/fp/basic.lean
0.0005323308270676691 src/control/bitraversable/lemmas.lean
0.0005312400888043134 test/ring_exp.lean
0.0005249662618083671 src/data/option/basic.lean
0.0005202639019792648 src/algebra/midpoint.lean
0.0005091705447577334 src/category_theory/limits/opposites.lean
0.0005070357018257937 src/order/lexicographic.lean
0.0005058717253839205 src/topology/order.lean
0.0005014097386268384 src/order/zorn.lean
0.0004931237721021611 src/data/set/intervals/unordered_interval.lean
0.0004901277584204413 src/control/bifunctor.lean
0.00048790058862001307 src/algebra/group_with_zero_power.lean
0.00048686244204018545 src/algebra/free.lean
0.0004831867854032643 src/order/complete_lattice.lean
0.00048018949181739877 src/algebra/group_ring_action.lean
0.0004783405605972551 src/data/equiv/local_equiv.lean
0.00047271487039563437 src/tactic/omega/eq_elim.lean
0.0004716887252462932 src/data/list/forall2.lean
0.00046905940594059404 src/logic/embedding.lean
0.0004602654714704361 src/category_theory/conj.lean
0.0004528841569998411 src/tactic/omega/int/dnf.lean
0.0004410453391865011 src/control/fold.lean
0.0004369294163617634 src/data/equiv/basic.lean
0.0004351823475329451 src/order/boolean_algebra.lean
0.0004298334025019268 src/order/bounded_lattice.lean
0.0004254694835680751 src/control/basic.lean
0.00042194791011682163 src/tactic/norm_num.lean
0.0004170616113744076 src/category_theory/action.lean
0.0004155005382131324 src/algebra/continued_fractions/terminated_stable.lean
0.0004146315752486033 src/group_theory/bundled_subgroup.lean
0.000413829693164736 src/topology/stone_cech.lean
0.00041319796954314723 src/data/list/chain.lean
0.00041287386215864755 src/set_theory/zfc.lean
0.00040857142857142855 src/linear_algebra/direct_sum_module.lean
0.00040386803185437996 src/category_theory/isomorphism.lean
0.00039965743648301454 docs/tutorial/category_theory/calculating_colimits_in_Top.lean
0.0003984431015056847 src/algebra/group/basic.lean
0.00038001273074474856 src/data/nat/gcd.lean
0.0003758618133293795 src/data/pnat/basic.lean
0.0003741293532338308 test/local_cache.lean
0.00036929057337220603 src/topology/homeomorph.lean
0.00036736323705577003 src/data/seq/computation.lean
0.0003611216438257227 src/tactic/ring_exp.lean
0.00035669474816275317 src/category_theory/concrete_category/bundled_hom.lean
0.0003555649063749211 src/data/equiv/ring.lean
0.0003532277710109622 src/algebra/char_zero.lean
0.00035009085402786194 src/ring_theory/subring.lean
0.0003495217071376012 src/tactic/monotonicity/basic.lean
0.0003423787097256485 src/order/galois_connection.lean
0.000339881509198628 src/category_theory/full_subcategory.lean
0.00033675953475791184 src/category_theory/limits/creates.lean
0.00032117506500808213 src/data/list/pairwise.lean
0.0003095104108047271 test/equiv_rw.lean
0.0002958933191799907 src/set_theory/surreal.lean
0.00029391304347826084 src/data/list/nodup.lean
0.00029381443298969075 src/tactic/tauto.lean
0.0002903778519253314 src/algebra/group/hom.lean
0.0002880859375 src/data/prod.lean
0.000276783583870198 src/tactic/omega/nat/neg_elim.lean
0.0002748126277538042 src/analysis/ODE/gronwall.lean
0.00027424308907415536 src/data/set/function.lean
0.00025075384859546103 src/tactic/omega/int/main.lean
0.0002482783617252628 src/order/filter/lift.lean
0.0002464827134911113 src/algebra/semiconj.lean
0.000242276061346966 src/tactic/omega/nat/main.lean
0.00023904382470119523 src/data/option/defs.lean
0.00023838524447537847 src/tactic/omega/nat/sub_elim.lean
0.00022624132407901763 src/algebra/commute.lean
0.00021896917305496658 src/order/bounds.lean
0.0002133697708639899 src/algebra/order.lean
0.00019927107492781747 src/group_theory/congruence.lean
0.0001838485632575242 src/control/monad/writer.lean
0.0001809285389167046 src/order/fixed_points.lean
0.0001755628792312194 src/order/basic.lean
0.0001644936325045482 src/logic/relation.lean
0.00016181229773462783 src/data/equiv/mul_add.lean
0.00015212066520562073 src/algebra/group/units.lean
0.00013499701899327143 src/tactic/monotonicity/interactive.lean
0.00013253159896919867 src/data/setoid.lean
0.00012844249016431383 src/tactic/simps.lean
0.00012643864483708869 src/logic/function.lean
0.00011602115679918104 src/tactic/ext.lean
0.0001092767757476059 src/control/traversable/derive.lean
0.00010299977445304866 src/algebra/continued_fractions/basic.lean
0.00010164607955606541 src/logic/basic.lean
9.740001590204342e-05 src/tactic/norm_cast.lean
8.166533226581265e-05 src/deprecated/group.lean
6.2672493100276e-05 src/tactic/suggest.lean
6.201474681380927e-05 src/data/list/defs.lean
5.3625053625053626e-05 src/order/filter/extr.lean
5.311203319502075e-05 src/tactic/interactive.lean
5.1278993500685704e-05 src/tactic/core.lean
4.416540376704915e-05 src/tactic/finish.lean
4.4142101284958426e-05 src/meta/expr.lean
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment