Last active
August 11, 2020 21:54
-
-
Save ammkrn/dab311e0d2d27b3bcd15ec6c4a2b019d to your computer and use it in GitHub Desktop.
mathlib_high_scores
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
#### SIZE (GARBAGE LEAN OBJECTS) | |
10794778 : polynomial.monic.next_coeff_mul | |
1090313 : composition_as_set_equiv._proof_5 | |
662922 : real.pi_lt_3141593 | |
468943 : real.pi_gt_3141592 | |
413365 : real.pi_lt_31416 | |
342992 : sum_range_choose_halfway | |
315037 : _private.4086404821.sum_four_squares_of_two_mul_sum_four_squares | |
263176 : polynomial.irreducible_of_eisenstein_criterion | |
228696 : AddCommGroup.kernel_iso_ker_over._proof_4 | |
227551 : composition_as_set_equiv._proof_6 | |
226028 : exp_neg_inv_glue.f_aux_deriv | |
225619 : AddCommGroup.kernel_iso_ker_over._proof_3 | |
225117 : continuous_equiv_fun_basis | |
184318 : multilinear_map.map_sum_finset_aux | |
183416 : real.pi_gt_31415 | |
174309 : Gromov_Hausdorff.totally_bounded | |
162194 : string.iterator.curr._main.equations._eqn_1 | |
159787 : composition_as_set_equiv._proof_2 | |
155768 : free_abelian_group.is_lawful_monad.equations._eqn_1 | |
155751 : free_abelian_group.is_lawful_monad | |
153638 : category_theory.nat_trans.on_presheaf._proof_1 | |
149583 : Module.monoidal_category.pentagon | |
143370 : category_theory.limits.prod_functor._proof_9 | |
138277 : Top.CommRing_yoneda._proof_8 | |
135271 : _private.433596857.prime_sum_four_squares | |
127140 : lift_of_splits | |
122671 : algebraic_geometry.PresheafedSpace.stalk_map.comp | |
122095 : polynomial.coeff_comp_degree_mul_degree | |
119313 : free_group.is_lawful_monad.equations._eqn_1 | |
119296 : free_group.is_lawful_monad | |
110915 : CommRing.category_theory.creates_limit.equations._eqn_1 | |
110883 : CommRing.category_theory.creates_limit | |
109156 : list.is_lawful_monad.equations._eqn_1 | |
109139 : list.is_lawful_monad | |
106545 : _private.3149472077.glue_dist_triangle | |
106049 : formal_multilinear_series.comp_summable_nnreal | |
105882 : times_cont_mdiff_on.times_cont_mdiff_on_tangent_map_within_aux | |
105228 : measure_theory.simple_func_sequence_tendsto | |
103917 : basic_smooth_bundle_core.to_smooth_manifold.equations._eqn_1 | |
103862 : basic_smooth_bundle_core.to_smooth_manifold | |
102778 : Gromov_Hausdorff.complete_space.equations._eqn_1 | |
102777 : gaussian_int.prime_of_nat_prime_of_mod_four_eq_three | |
102761 : Gromov_Hausdorff.complete_space | |
101996 : has_fpower_series_at.comp | |
101877 : real.pi_gt_314 | |
101616 : Module.monoidal_category.associator_naturality | |
101475 : CommRing.category_theory.creates_limit._proof_10 | |
100051 : AddCommGroup.kernel_iso_ker._proof_6 | |
99331 : real.sin_bound | |
99085 : measure_theory.hahn_decomposition | |
98735 : complex.exists_root | |
98406 : times_cont_mdiff_on.times_cont_mdiff_on_tangent_map_within | |
98058 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_42 | |
97954 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_44 | |
96955 : real.exists_sup | |
96492 : ring.direct_limit.of.zero_exact_aux | |
95623 : filter.is_lawful_monad | |
94929 : Gromov_Hausdorff.second_countable.equations._eqn_1 | |
94912 : Gromov_Hausdorff.second_countable | |
94452 : set.is_lawful_monad.equations._eqn_1 | |
94435 : set.is_lawful_monad | |
94385 : category_theory.functor.map_presheaf._proof_2 | |
93352 : Module.monoidal_category.triangle | |
93068 : exists_approx_preimage_norm_le | |
92918 : real.cos_bound | |
92117 : Top.CommRing_yoneda.equations._eqn_1 | |
92097 : Top.CommRing_yoneda | |
92068 : AddCommGroup.kernel_iso_ker_inv_comp_ι | |
91835 : _private.217157525.is_st_mul' | |
91611 : primorial_le_4_pow | |
89980 : has_ftaylor_series_up_to_on_succ_iff_right | |
89586 : norm_eq_infi_iff_inner_le_zero | |
89526 : is_bounded_linear_map_prod_multilinear | |
89465 : pythagorean_triple.is_primitive_classified_of_coprime_of_odd_of_pos | |
88440 : _private.1179974605.make_monospaced._main.equations._eqn_3 | |
88374 : _private.1179974605.make_monospaced._main.equations._eqn_2 | |
88246 : _private.1179974605.make_monospaced._main.equations._eqn_1 | |
87963 : gaussian_int.euclidean_domain._proof_1 | |
87247 : real.continuous_rpow_aux3 | |
86417 : real.pi_lt_315 | |
86056 : Top.presheaf.stalk_pushforward.comp | |
85927 : Icc_smooth_manifold.equations._eqn_1 | |
85898 : Icc_smooth_manifold | |
85580 : semiquot.is_lawful_monad.equations._eqn_1 | |
85563 : semiquot.is_lawful_monad | |
85387 : exists_norm_eq_infi_of_complete_convex | |
85127 : normed_field.tendsto_inv | |
84453 : is_bounded_bilinear_map_comp_multilinear | |
84254 : linear_map.continuous_iff_is_closed_ker | |
84245 : inner_product_geometry.angle_add_angle_sub_add_angle_sub_eq_pi | |
83918 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_43 | |
82885 : half_le_harmonic_double_sub_harmonic | |
82589 : formal_multilinear_series.change_origin_radius | |
82247 : dense_Inter_of_open_nat | |
81360 : has_ftaylor_series_up_to_on.prod | |
80199 : real.abs_log_sub_add_sum_range_le | |
80135 : category_theory.limits.cocones.whiskering_equivalence._proof_5 | |
79468 : formal_multilinear_series.bound_of_lt_radius | |
78647 : is_noetherian_pi.equations._eqn_1 | |
78600 : is_noetherian_pi | |
#### TIME (MILLISECONDS) | |
7584 : polynomial.monic.next_coeff_mul | |
684 : composition_as_set_equiv._proof_5 | |
353 : Gromov_Hausdorff.totally_bounded | |
346 : real.pi_lt_3141593 | |
233 : real.pi_gt_3141592 | |
213 : real.pi_lt_31416 | |
204 : _private.4086404821.sum_four_squares_of_two_mul_sum_four_squares | |
190 : sum_range_choose_halfway | |
183 : real.exists_sup | |
179 : lift_of_splits | |
174 : AddCommGroup.kernel_iso_ker_over._proof_4 | |
172 : pythagorean_triple.is_primitive_classified_of_coprime_of_odd_of_pos | |
171 : AddCommGroup.kernel_iso_ker_over._proof_3 | |
165 : polynomial.irreducible_of_eisenstein_criterion | |
161 : continuous_equiv_fun_basis | |
153 : exists_approx_preimage_norm_le | |
153 : _private.217157525.is_st_mul' | |
150 : cauchy_product | |
146 : exp_neg_inv_glue.f_aux_deriv | |
143 : norm_eq_infi_iff_inner_le_zero | |
136 : complex.sum_div_fact_le | |
135 : real.continuous_rpow_aux3 | |
132 : normed_field.tendsto_inv | |
131 : hofer | |
129 : real.pi_lt_sqrt_two_add_series | |
128 : Gromov_Hausdorff.second_countable.equations._eqn_1 | |
128 : Gromov_Hausdorff.second_countable | |
124 : _private.433596857.prime_sum_four_squares | |
124 : real.sin_bound | |
122 : complex.exists_root | |
122 : measure_theory.hahn_decomposition | |
121 : discriminant_le_zero | |
120 : linear_map.continuous_iff_is_closed_ker | |
119 : composition_as_set_equiv._proof_6 | |
116 : half_le_harmonic_double_sub_harmonic | |
115 : category_theory.limits.prod_functor._proof_9 | |
115 : real.cos_bound | |
112 : free_abelian_group.is_lawful_monad | |
112 : real.abs_log_sub_add_sum_range_le | |
111 : normed_ring.inverse_one_sub_norm | |
111 : real.sin_pos_of_pos_of_le_one | |
111 : exists_norm_eq_infi_of_complete_convex | |
110 : free_abelian_group.is_lawful_monad.equations._eqn_1 | |
109 : formal_multilinear_series.comp_summable_nnreal | |
107 : real.sqrt_exists | |
107 : real.pi_gt_31415 | |
105 : measure_theory.simple_func_sequence_tendsto | |
105 : _private.3149472077.glue_dist_triangle | |
104 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_44 | |
100 : subset_tangent_cone_prod_right | |
100 : subset_tangent_cone_prod_left | |
100 : real.cos_pi_over_two_pow | |
98 : exists_preimage_norm_le | |
96 : multilinear_map.exists_bound_of_continuous | |
94 : category_theory.nat_trans.on_presheaf._proof_1 | |
94 : multilinear_map.map_sum_finset_aux | |
93 : isometric.midpoint_fixed | |
93 : algebraic_geometry.PresheafedSpace.stalk_map.comp | |
92 : convex_on_real_of_slope_mono_adjacent | |
92 : real.sin_gt_sub_cube | |
91 : real.cos_pos_of_le_one | |
91 : hyperreal.is_st_neg | |
89 : exists_rat_btwn | |
89 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_42 | |
88 : continuous_multilinear_map.continuous_eval | |
88 : mem_tangent_cone_of_segment_subset | |
88 : self_div_two_le_harmonic_two_pow | |
87 : Gromov_Hausdorff.complete_space.equations._eqn_1 | |
86 : has_fpower_series_at.comp | |
86 : fpow_strict_mono | |
86 : Gromov_Hausdorff.complete_space | |
85 : hyperreal.infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos | |
85 : Icc_smooth_manifold.equations._eqn_1 | |
85 : rescale_to_shell | |
84 : Icc_smooth_manifold | |
84 : mem_pos_tangent_cone_at_of_segment_subset | |
84 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_43 | |
83 : real.sin_lt | |
82 : real.cos_lt_cos_of_nonneg_of_le_pi | |
82 : real.cos_lt_cos_of_nonneg_of_le_pi_div_two | |
82 : gaussian_int.norm_sq_div_sub_div_lt_one | |
81 : complex.is_cau_abs_exp | |
81 : inner_product_geometry.angle_add_angle_sub_add_angle_sub_eq_pi | |
80 : free_group.is_lawful_monad.equations._eqn_1 | |
80 : formal_multilinear_series.change_origin_radius | |
80 : Top.CommRing_yoneda._proof_8 | |
79 : riesz_extension.step | |
79 : riesz_lemma | |
79 : free_group.is_lawful_monad | |
79 : CommRing.category_theory.creates_limit | |
78 : CommRing.category_theory.creates_limit.equations._eqn_1 | |
78 : primorial_le_4_pow | |
78 : complex.abs_exp_sub_one_sub_id_le | |
77 : basic_smooth_bundle_core.to_smooth_manifold.equations._eqn_1 | |
77 : complex.cpow_nat_inv_pow | |
77 : is_cau_geo_series | |
76 : abs_sub_round | |
75 : sum_bernoulli | |
75 : hyperreal.is_st_add | |
75 : basic_smooth_bundle_core.to_smooth_manifold | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment