Last active
July 20, 2022 07:21
-
-
Save jcommelin/90b42c047ec1959abe8a359ae5fd0d57 to your computer and use it in GitHub Desktop.
Treeshaking LTE e02550056c896599ed0731b93c0e868124b62e88
This file contains hidden or 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
| AddCommGroup.Ab.category_theory.limits.has_colimits_of_size | |
| AddCommGroup.colimit_comparison | |
| AddCommGroup.direct_sum_bicone | |
| AddCommGroup.direct_sum_punit_iso | |
| AddCommGroup.hom_product_comparison | |
| AddCommGroup.is_bilimit_direct_sum_bicone | |
| AddCommGroup.is_iso_hom_product_comparison | |
| AddCommGroup.is_limit_pi_fan | |
| AddCommGroup.pi_fan | |
| AddCommGroup.pi_lift | |
| AddCommGroup.pi_π | |
| AddCommGroup.tensor_functor_flip_additive | |
| AddCommGroup.to_direct_sum | |
| add_equiv.quotient_congr | |
| add_monoid_hom.mk_from_pi | |
| add_monoid_hom.mk_polyhedral_lattice_hom' | |
| add_monoid_hom.pow | |
| add_monoid_hom.pow_hom | |
| as_normed_space' | |
| as_normed_space'.add_comm_group | |
| as_normed_space'.down | |
| as_normed_space'.has_norm | |
| as_normed_space'.inhabited | |
| as_normed_space'.module | |
| as_normed_space'.normed_group | |
| as_normed_space'.normed_space' | |
| as_normed_space'.up | |
| aux_thm69.equiv_bdd_integer_nat | |
| aux_thm69.equiv_compl_R_bdd | |
| aux_thm69.equiv.group_mul | |
| aux_thm69.equiv_Icc_bdd_nonneg | |
| aux_thm69.equiv_Icc_R | |
| aux_thm69.equiv.le_one_ge_one | |
| aux_thm69.equiv.lt_one_gt_one | |
| aux_thm69.equiv.mul_inv | |
| aux_thm69.equiv_nat_diag | |
| aux_thm69.int.nonneg_equiv_nat | |
| aux_thm69.mul_inv_fun | |
| aux_thm69.nat.le_equiv_nat | |
| aux_thm69.R | |
| aux_thm69.range_equiv_Icc | |
| aux_thm69.T | |
| bicartesian.biprod.matrix | |
| bicartesian.quatro_cone | |
| bicartesian.quatro_cone_acyclic | |
| bicartesian.quatro_cons | |
| bicartesian.quatro_cons_acyclic | |
| bicartesian.quatro_cons_hom | |
| bicartesian.quatro_cons_hom_quasi_iso | |
| bounded_derived_category.additive | |
| bounded_derived_category.category_theory.category | |
| bounded_derived_category.cone | |
| bounded_derived_category.Ext | |
| bounded_derived_category.Ext_additive_fst | |
| bounded_derived_category.Ext_homological_fst | |
| bounded_derived_category.forget | |
| bounded_derived_category.forget.category_theory.faithful | |
| bounded_derived_category.forget.category_theory.full | |
| bounded_derived_category.forget_replace_triangle | |
| bounded_derived_category.forget_triangulated_functor_struct | |
| bounded_derived_category.has_shift_functor | |
| bounded_derived_category.has_shift_functor_forget | |
| bounded_derived_category.has_zero_object | |
| bounded_derived_category.int.category_theory.has_shift | |
| bounded_derived_category.lift | |
| bounded_derived_category.lift_unique | |
| bounded_derived_category.localization_functor | |
| bounded_derived_category.localization_iso | |
| bounded_derived_category.localize_lift | |
| bounded_derived_category.mk_iso | |
| bounded_derived_category.of | |
| bounded_derived_category.preadditive | |
| bounded_derived_category.pretriangulated | |
| bounded_derived_category.pretriangulated_distinguished_triangles | |
| bounded_derived_category.replace_triangle | |
| bounded_derived_category.replace_triangle' | |
| bounded_derived_category.replace_triangle_map | |
| bounded_derived_category.replace_triangle_rotate | |
| bounded_derived_category.shift_functor_forget | |
| bounded_derived_category.shift_functor_localization_functor | |
| bounded_derived_category.val.homotopy_category.is_K_projective | |
| bounded_derived_category.zero | |
| bounded_homotopy_category.e | |
| bounded_homotopy_category.forget_shift | |
| bounded_homotopy_category.hom_shift_left_iso | |
| bounded_homotopy_category.hom_shift_right_iso | |
| bounded_homotopy_category.hom_val | |
| bounded_homotopy_category.obj.category_theory.triangulated.homological_functor | |
| bounded_homotopy_category.preserves_coproducts_single | |
| bounded_homotopy_category.shift_equiv_inverse_additive | |
| bounded_homotopy_category.shift_equiv_symm_inverse_additive | |
| bounded_homotopy_category.shift_of_eq | |
| bounded_homotopy_category.single_forget | |
| bounded_homotopy_category.val_as_bdd_above | |
| breen_deligne.basic_universal_map.eval | |
| breen_deligne.basic_universal_map.pre_eval | |
| breen_deligne.basic_universal_map.suitable_mul_left_le_one | |
| breen_deligne.basic_universal_map.suitable_mul_left_one_le | |
| breen_deligne.basic_universal_map.suitable_mul_right_le_one | |
| breen_deligne.basic_universal_map.suitable_mul_right_one_le | |
| breen_deligne.data.additive_whiskering_left | |
| breen_deligne.data.additive_whiskering_right | |
| breen_deligne.data.complex_d | |
| breen_deligne.data.complex_X | |
| breen_deligne.data.comp_suitable | |
| breen_deligne.data.eval_functor'_comp | |
| breen_deligne.data.eval_functor_comp | |
| breen_deligne.data.hom_pow'_suitable_strict | |
| breen_deligne.data.preadditive | |
| breen_deligne.data.proj_suitable | |
| breen_deligne.FreeMat.to_FreeAbMat | |
| breen_deligne.Mat | |
| breen_deligne.Mat.category_theory.small_category | |
| breen_deligne.Mat.comm_semiring | |
| breen_deligne.package.eval'_bounded_above | |
| breen_deligne.package.eval_homotopy | |
| breen_deligne.package.hH0_endo | |
| breen_deligne.package.hH0_endo₂ | |
| breen_deligne.universal_map.eval | |
| breen_deligne.universal_map.eval_Pow' | |
| breen_deligne.universal_map.suitable_mul_left_le_one | |
| breen_deligne.universal_map.suitable_mul_left_one_le | |
| breen_deligne.universal_map.suitable_mul_right_le_one | |
| breen_deligne.universal_map.suitable_mul_right_one_le | |
| breen_deligne.universal_map.suitable_neg | |
| breen_deligne.universal_map.suitable_sub | |
| breen_deligne.universal_map.very_suitable.mul_right | |
| category_theory.additive_equivalence_inverse | |
| category_theory.adjunction.preadditive_yoneda_whiskering_left | |
| category_theory.adjunction.whiskering_right | |
| category_theory.adjunction.yoneda_whiskering_left | |
| category_theory.arrow.contracting_homotopy' | |
| category_theory.arrow.op | |
| category_theory.biprod.is_biprod | |
| category_theory.colimit_homology_functor_iso | |
| category_theory.composable_morphisms.apply_functor | |
| category_theory.composable_morphisms.hom.inhabited | |
| category_theory.composable_morphisms.inhabited | |
| category_theory.cosimplicial_object.cocomplex | |
| category_theory.cosimplicial_object.to_cocomplex | |
| category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting_sheafification_compatibility | |
| category_theory.endomorphisms.free.map | |
| category_theory.endomorphisms.functor.free | |
| category_theory.endomorphisms.functor.free_additive | |
| category_theory.endomorphisms.has_colimits | |
| category_theory.endomorphisms.has_limits | |
| category_theory.endomorphisms.kernel_fork_iso | |
| category_theory.endomorphisms.mk_bo_ha_ca'_single | |
| category_theory.endomorphisms.mk_bo_ha_ca_single | |
| category_theory.endomorphisms.mk_bo_ho_ca | |
| category_theory.endomorphisms.mk_bo_ho_ca' | |
| category_theory.endomorphisms.preadditive_yoneda_flip_additive | |
| category_theory.endomorphisms.preserves_colimits | |
| category_theory.endomorphisms.preserves_limits | |
| category_theory.endomorphisms.single_unEnd | |
| category_theory.eval_functor_colimit_iso | |
| category_theory.functor.finite_product_aux.obj_equiv | |
| category_theory.functor.finite_product_condition' | |
| category_theory.functor.flip_evaluation_comp_whiskering_right | |
| category_theory.functor.forget₂_additive | |
| category_theory.functor.homology_iso | |
| category_theory.functor.is_proetale_sheaf_of_types_projective | |
| category_theory.functor.map_commsq | |
| category_theory.functor.map_is_biprod | |
| category_theory.functor.obj_biprod_iso | |
| category_theory.functor.pbool.fintype | |
| category_theory.functor.preserves_coequalizers_of_exact | |
| category_theory.functor.preserves_finite_colimits_of_exact | |
| category_theory.functor.single | |
| category_theory.functor.whiskering_right_obj_comp | |
| category_theory.homology_functor_preserves_filtered_colimits | |
| category_theory.homology_iso_inv_homology_functor_map | |
| category_theory.is_biprod.iso_biprod | |
| category_theory.is_iso_sheafification_types_adjunction_counit_app | |
| category_theory.is_snake_input.aux_simp | |
| category_theory.is_snake_input.cokernel_to' | |
| category_theory.is_snake_input.cokernel_to'_mono | |
| category_theory.is_snake_input.to_kernel' | |
| category_theory.is_snake_input.to_kernel_epi | |
| category_theory.limits.cofork_of_cokernel | |
| category_theory.limits.cofork_of_cokernel_is_colimit | |
| category_theory.limits.is_limit_op_fan | |
| category_theory.limits.op_fan | |
| category_theory.limits.preserves_zero_of_preserves_initial | |
| category_theory.nat_iso.unflip | |
| category_theory.nat_trans.conj_by | |
| category_theory.nat_trans.unflip | |
| category_theory.preadditive.eval_Pow_functor_comp | |
| category_theory.preadditive.Pow.category_theory.limits.preserves_colimits | |
| category_theory.presheaf_to_SheafOfTypes | |
| category_theory.presheaf_to_SheafOfTypes_iso | |
| category_theory.projective.category_theory.limits.factor_thru_image.category_theory.strong_epi | |
| category_theory.projective.f.category_theory.epi | |
| category_theory.projective.homology.ι.category_theory.mono | |
| category_theory.projective.pullback_comp_mono_iso | |
| category_theory.ProjectiveResolution.epi_hom_to_kernel | |
| category_theory.ProjectiveResolution.Ext_iso_zero | |
| category_theory.ProjectiveResolution.Ext_single_iso | |
| category_theory.ProjectiveResolution.Ext_single_iso_kernel | |
| category_theory.ProjectiveResolution.homology_zero_iso | |
| category_theory.ProjectiveResolution.hom_to_kernel | |
| category_theory.ProjectiveResolution.is_iso_hom_to_kernel | |
| category_theory.ProjectiveResolution.mono_hom_to_kernel | |
| category_theory.projective.snd.category_theory.epi | |
| category_theory.sheafification_adjunction_types | |
| category_theory.sheafification_types_reflective | |
| category_theory.short_exact_sequence.aux_tac | |
| category_theory.short_exact_sequence.category_theory.category | |
| category_theory.short_exact_sequence.category_theory.limits.has_zero_morphisms | |
| category_theory.short_exact_sequence.category_theory.preadditive | |
| category_theory.short_exact_sequence.comp | |
| category_theory.short_exact_sequence.f_nat | |
| category_theory.short_exact_sequence.Fst | |
| category_theory.short_exact_sequence.Fst_additive | |
| category_theory.short_exact_sequence.functor | |
| category_theory.short_exact_sequence.Functor | |
| category_theory.short_exact_sequence.functor_map | |
| category_theory.short_exact_sequence.g_nat | |
| category_theory.short_exact_sequence.has_nsmul | |
| category_theory.short_exact_sequence.has_zsmul | |
| category_theory.short_exact_sequence.hom_inj | |
| category_theory.short_exact_sequence.id | |
| category_theory.short_exact_sequence.iso_of_components | |
| category_theory.short_exact_sequence.iso_of_components' | |
| category_theory.short_exact_sequence.left_split | |
| category_theory.short_exact_sequence.left_split.splitting | |
| category_theory.short_exact_sequence.mk_of_split | |
| category_theory.short_exact_sequence.mk_of_split' | |
| category_theory.short_exact_sequence.mk_split | |
| category_theory.short_exact_sequence.quiver | |
| category_theory.short_exact_sequence.quiver.hom.has_add | |
| category_theory.short_exact_sequence.quiver.hom.has_neg | |
| category_theory.short_exact_sequence.quiver.hom.has_sub | |
| category_theory.short_exact_sequence.right_split | |
| category_theory.short_exact_sequence.right_split.splitting | |
| category_theory.short_exact_sequence.Snd | |
| category_theory.short_exact_sequence.Snd_additive | |
| category_theory.short_exact_sequence.split | |
| category_theory.short_exact_sequence.Trd | |
| category_theory.short_exact_sequence.Trd_additive | |
| category_theory.sigma_functor_preserves_epi | |
| category_theory.sigma_functor_preserves_mono | |
| category_theory.simplicial_object.augmented.complex | |
| category_theory.simplicial_object.complex | |
| category_theory.simplicial_object.to_complex | |
| category_theory.snake_diagram.decidable_eq | |
| category_theory.snake_diagram.hom_tac | |
| category_theory.snake_diagram.map_tac | |
| category_theory.snake_diagram.mk_functor' | |
| category_theory.snake_diagram.mk_functor'' | |
| category_theory.snake_diagram.mk_of_short_exact_sequence_hom | |
| category_theory.snake_input.category_theory.category | |
| category_theory.snake_input.kernel_sequence | |
| category_theory.snake_input.mk_of_short_exact_sequence_hom | |
| category_theory.snake_input.proj | |
| category_theory.snake_lemma.δ | |
| category_theory.snake.snake_input | |
| category_theory.splitting.retraction.category_theory.epi | |
| category_theory.splitting.section.category_theory.mono | |
| category_theory.triangulated.linear_yoneda_flip_additive | |
| category_theory.triangulated.linear_yoneda_flip_homological | |
| category_theory.triangulated.triangle.obj₁_functor | |
| category_theory.triangulated.triangle.obj₂_functor | |
| category_theory.triangulated.triangle.obj₃_functor | |
| chain_complex_embed_cofan_iso | |
| chain_complex_embed_cofan_uniformly_bounded | |
| chain_complex.is_projective_resolution.mk_ProjectiveResolution | |
| chain_complex_nat_has_homology | |
| chain_complex_nat_has_homology_0 | |
| chain_complex_to_bounded_homotopy_category_preserves_coproducts | |
| CLCFP.T | |
| CLCTinv.map_nat_iso | |
| cochain_complex.cons | |
| cochain_complex.cons.d | |
| cochain_complex.cons.X | |
| cochain_complex.hom.cons | |
| cochain_complex.hom.cons.f | |
| cochain_complex.imker.homology_zero_zero' | |
| cochain_complex.imker.X_iso_kernel | |
| cochain_complex_int_has_homology | |
| combinatorial_lemma.recursion_data.inhabited | |
| CompHaus.category_theory.forget.category_theory.limits.preserves_limits | |
| comphaus_filtered_pseudo_normed_group_hom.inhabited | |
| comphaus_filtered_pseudo_normed_group_hom.strict.to_schfpsng_hom | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.has_zero | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.inhabited | |
| CompHausFiltPseuNormGrp₁.rescale_to_Condensed_iso | |
| CompHausFiltPseuNormGrp₁.to_PNG₁.category_theory.faithful | |
| CompHausFiltPseuNormGrp₁.to_PNG₁.category_theory.limits.preserves_limits | |
| CompHausFiltPseuNormGrp.rescale₁ | |
| CompHausFiltPseuNormGrp.rescale_preserves_limits_of_shape_discrete_quotient | |
| CompHausFiltPseuNormGrpWithTinv | |
| CompHausFiltPseuNormGrpWithTinv.concrete_category | |
| CompHausFiltPseuNormGrpWithTinv.has_coe_to_sort | |
| CompHausFiltPseuNormGrpWithTinv.large_category | |
| complex_shape.embedding.nat_up_int_up | |
| Condensed.AB5 | |
| Condensed_Ab_to_CondensedSet_preserves_limits_of_shape_of_filtered | |
| Condensed.category_theory.endomorphisms.category_theory.enough_projectives | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_coproducts_of_shape | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_finite_biproducts | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_finite_colimits | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_finite_limits | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_products_of_shape | |
| Condensed.category_theory.limits.has_colimits | |
| Condensed.category_theory.limits.has_limits | |
| Condensed.category_theory.Sheaf_to_presheaf.category_theory.is_right_adjoint | |
| Condensed.coproduct_presentation | |
| Condensed.eval_freeAb_iso | |
| Condensed.eval_freeCond'_iso | |
| Condensed.evaluation_additive | |
| Condensed.forget_to_CondensedType | |
| Condensed.forget_to_CondensedType.category_theory.is_right_adjoint | |
| Condensed.half_internal_hom | |
| Condensed.half_internal_hom_eval_iso | |
| Condensed.half_internal_hom_iso | |
| Condensed.homology_evaluation_iso | |
| Condensed.homology_functor_evaluation_iso | |
| Condensed.presentation_point_isomorphism | |
| Condensed.preserves_finite_limits | |
| condensed.Profinite_to_presheaf_Ab | |
| CondensedSet.evaluation.category_theory.limits.preserves_limits | |
| CondensedSet.is_colimit_sigma_cone | |
| CondensedSet.sigma_cone | |
| Condensed.tensor_curry | |
| Condensed.tensor_eval_iso | |
| Condensed.tensor_iso | |
| Condensed.tensor_uncurry | |
| condensed.unsheafified_free_Cech' | |
| condensify_def | |
| coproduct_eval_iso | |
| embed_coproduct_iso | |
| embed_unop | |
| exact_notation | |
| ExtrDisc.binary_product_condition | |
| ExtrDisc.compact_space | |
| ExtrDisc.empty | |
| ExtrDisc.empty.elim | |
| ExtrDisc.of | |
| ExtrDisc.sum | |
| ExtrDisc.sum.desc | |
| ExtrDisc.sum.inl | |
| ExtrDisc.sum.inr | |
| ExtrDisc.t2_space | |
| ExtrDisc.terminal_condition | |
| ExtrDisc.topological_space | |
| ExtrDisc.totally_disconnected_space | |
| ExtrSheaf.half_internal_hom | |
| ExtrSheafProd.evaluation | |
| ExtrSheafProd.evaluation_additive | |
| ExtrSheafProd.half_internal_hom | |
| ExtrSheafProd.hom_has_add | |
| ExtrSheafProd.hom_has_neg | |
| ExtrSheafProd.hom_has_sub | |
| ExtrSheafProd.hom_has_zero | |
| ExtrSheafProd.preadditive | |
| ExtrSheafProd.tensor_curry | |
| ExtrSheafProd.tensor_functor | |
| ExtrSheafProd.tensor_functor_additive | |
| ExtrSheafProd.tensor_functor_flip_additive | |
| ExtrSheafProd.tensor_uncurry | |
| ExtrSheaf.tensor_curry | |
| ExtrSheaf.tensor_functor_additive | |
| ExtrSheaf.tensor_uncurry | |
| Filtration.pi_iso | |
| Filtration.res | |
| Fintype.LaurentMeasure | |
| Fintype.normed_free_pfpng | |
| Fintype.normed_free_pfpng_unit | |
| first_target_stmt | |
| has_homology.fst_eq_zero | |
| has_homology.fst_snd_eq_zero | |
| has_homology.snd_eq_zero | |
| has_lt.lt.fact | |
| homological_complex.biproduct_bicone | |
| homological_complex.biproduct_bicone_is_coprod | |
| homological_complex.biproduct_bicone_is_prod | |
| homological_complex.biproduct.desc | |
| homological_complex.biproduct.inr | |
| homological_complex.biproduct_is_biprod | |
| homological_complex.biproduct.snd | |
| homological_complex.boundaries_map.category_theory.epi | |
| homological_complex.category_theory.limits.has_binary_biproducts | |
| homological_complex.category_theory.limits.has_colimits_of_shape | |
| homological_complex.category_theory.limits.has_colimits_of_size | |
| homological_complex.category_theory.limits.has_limits_of_size | |
| homological_complex.cone.desc_of_null_homotopic | |
| homological_complex.cone_from_zero | |
| homological_complex.cone.lift_of_null_homotopic | |
| homological_complex.cone_to_termwise_split_comp_homotopy | |
| homological_complex.cone_to_zero | |
| homological_complex.cone.triangle_functorial | |
| homological_complex.cone.triangle_map | |
| homological_complex.embed.d_of_none_src | |
| homological_complex_embed_preserves_coproducts | |
| homological_complex.eval.category_theory.limits.preserves_colimits_of_size | |
| homological_complex.eval.category_theory.limits.preserves_limits_of_shape | |
| homological_complex.eval.category_theory.limits.preserves_limits_of_size | |
| homological_complex.eval_functor | |
| homological_complex.eval_functor_equiv | |
| homological_complex.eval_functor_homology_iso | |
| homological_complex.eval_functor.obj | |
| homological_complex.f.category_theory.split_epi | |
| homological_complex.functor_eval_homology_iso | |
| homological_complex.functor_eval_homology_nat_iso | |
| homological_complex_has_homology | |
| homological_complex.homological_complex.embed.subsingleton_to_none | |
| homological_complex.homotopy_connecting_hom_of_splittings | |
| homological_complex.kernel | |
| homological_complex.kernel.ι | |
| homological_complex.kernel.ι_mono | |
| homological_complex.obj.category_theory.limits.preserves_finite_colimits | |
| homological_complex.obj.category_theory.limits.preserves_finite_limits | |
| homological_complex.op_functor_additive | |
| homological_complex.shift_functor_additive | |
| homological_complex.single_obj_iso_zero | |
| homological_complex.termwise_split_epi_desc | |
| homological_complex.termwise_split_epi_lift | |
| homological_complex.termwise_split_epi_retraction | |
| homological_complex.termwise_split_epi_retraction_lift | |
| homological_complex.triangleₕ_map_splittings_hom | |
| homological_complex.triangleₕ_map_splittings_iso | |
| homological_complex.unop_functor_additive | |
| homology_embed_iso | |
| homology_iso_datum.change.coker_iso | |
| homology_iso_datum.change.tautological | |
| homology_iso_datum.change.η.category_theory.is_iso | |
| homology_iso_datum.change.κ.category_theory.is_iso | |
| homology_iso_datum.map_iso | |
| homology_iso_datum.of_homological_complex | |
| homology_iso_datum.of_homological_complex_of_next_eq_none | |
| homology_iso_datum.of_homological_complex_of_next_eq_none' | |
| homology_iso_datum.tautological | |
| homology_iso_datum.ι.category_theory.mono | |
| homology_iso_predatum.map_iso | |
| homology_iso_predatum.tautological | |
| homology_map_datum.of_g_are_zeros | |
| homotopy_category.is_quasi_iso_cone_π | |
| homotopy_category.quotient_op_functor | |
| homotopy_category.quotient_unop_functor | |
| homotopy_category.unop_functor | |
| invpoly.has_norm | |
| is_bounded_above_shift | |
| laurent_measures.condensed | |
| laurent_measures.condensedCH | |
| laurent_measures.nnreal.has_continuous_smul | |
| laurent_measures.profinite | |
| laurent_measures.profiniteCH | |
| laurent_measures.profinite_comp_PFPNGT₁_to_CHFPNG₁ₑₗ | |
| laurent_measures_ses.cfpng_hom_add | |
| laurent_measures_ses.cfpng_hom_neg | |
| laurent_measures_ses.comphaus_filtered_pseudo_normed_group_hom.add_comm_group | |
| laurent_measures_ses.Φ | |
| Lbar_bdd.has_zero | |
| Lbar_bdd.inhabited | |
| Lbar.inhabited | |
| Lbar_le.has_zero | |
| Lbar_le.inhabited | |
| Lbar.mk_aux' | |
| LCFP.obj.normed_with_aut | |
| LCFP.T | |
| liquid_tensor_experiment.sections | |
| locally_constant.has_edist | |
| locally_constant.metric_space | |
| locally_constant.normed_group | |
| locally_constant.uniform_space | |
| map_homological_complex_embed | |
| mul_equiv.quotient_congr | |
| mul_equiv.surjective_congr | |
| natural_fork | |
| nnrat.archimedean | |
| nnrat.can_lift | |
| nnrat.contravariant_add | |
| nnrat.covariant_add | |
| nnrat.covariant_mul | |
| nnrat.densely_ordered | |
| nnrat.gi | |
| nnrat.has_ordered_sub | |
| nnrat.inhabited | |
| nnreal.fact_inv_mul_le | |
| nnreal.fact_le_inv_mul_self | |
| nnreal.fact_le_subst_left' | |
| nnreal.fact_le_subst_right | |
| nnreal.fact_le_subst_right' | |
| nnreal.fact_nat_cast_inv_le_one | |
| nnreal.fact_one_le_add_one | |
| nnreal.fact_two_pow_inv_le_one | |
| normed_space.normed_space' | |
| of_epi_g | |
| pBanach.has_coe_to_fun_condensed_eval | |
| pBanach.has_continuous_smul | |
| PolyhedralLattice.category_theory.limits.has_zero_morphisms | |
| PolyhedralLattice.Cech_conerve.map_succ_zero | |
| PolyhedralLattice.Cech_conerve.map_succ_zero_aux | |
| PolyhedralLattice.Cech_conerve.π_hom | |
| PolyhedralLattice.Cech_conerve.π_hom.category_theory.epi | |
| polyhedral_lattice.filtration_fintype | |
| polyhedral_lattice_hom.has_zero | |
| polyhedral_lattice_hom.to_normed_group_hom | |
| polyhedral_lattice.profinitely_filtered_pseudo_normed_group | |
| PolyhedralLattice.rescale | |
| PolyhedralLattice.rescale_proj | |
| PolyhedralLattice.to_SemiNormedGroup | |
| PolyhedralLattice.unrescale | |
| Pow | |
| pow_equiv | |
| Pow_mul | |
| pow_pow | |
| Pow_Pow_X | |
| preserves_finite_biproducts_Condensed_evaluation | |
| preserves_limits_aux_1 | |
| preserves_limits_of_shape_of_filtered_aux | |
| presheaf_to_Condensed_Ab_preserves_colimits | |
| product_iso_biproduct | |
| ProFiltPseuNormGrp | |
| ProFiltPseuNormGrp₁.PFPNG₁_to_PFPNGₑₗ | |
| ProFiltPseuNormGrp₁.to_PNG₁.category_theory.faithful | |
| ProFiltPseuNormGrp.bundled_hom | |
| ProFiltPseuNormGrp.CompHausFiltPseuNormGrp.category_theory.has_forget₂ | |
| ProFiltPseuNormGrp.concrete_category | |
| ProFiltPseuNormGrp.has_coe_to_sort | |
| ProFiltPseuNormGrp.has_zero | |
| ProFiltPseuNormGrp.inhabited | |
| ProFiltPseuNormGrp.large_category | |
| ProFiltPseuNormGrp.of | |
| ProFiltPseuNormGrp.profinitely_filtered_pseudo_normed_group | |
| ProFiltPseuNormGrp.to_CompHausFilt | |
| ProFiltPseuNormGrp.Top.of.compact_space | |
| ProFiltPseuNormGrp.Top.of.t2_space | |
| ProFiltPseuNormGrp.Top.of.totally_disconnected_space | |
| ProFiltPseuNormGrpWithTinv₁.limit_cone_is_limit | |
| ProFiltPseuNormGrpWithTinv₁.obj.category_theory.limits.preserves_limits | |
| ProFiltPseuNormGrpWithTinv₁.PFPNGT₁_to_PFPNGTₑₗ | |
| ProFiltPseuNormGrpWithTinv₁.product | |
| ProFiltPseuNormGrpWithTinv₁.product.fan | |
| ProFiltPseuNormGrpWithTinv₁.product.is_limit | |
| ProFiltPseuNormGrpWithTinv₁.product.lift | |
| ProFiltPseuNormGrpWithTinv₁.product.π | |
| ProFiltPseuNormGrpWithTinv₁.rescale | |
| ProFiltPseuNormGrpWithTinv₁.rescale_out | |
| ProFiltPseuNormGrpWithTinv.has_zero | |
| ProFiltPseuNormGrpWithTinv.inhabited | |
| ProFiltPseuNormGrpWithTinv.Top.of.compact_space | |
| ProFiltPseuNormGrpWithTinv.Top.of.t2_space | |
| ProFiltPseuNormGrpWithTinv.Top.of.totally_disconnected_space | |
| Profinite.arrow_cone_iso | |
| Profinite.discrete_topology_pmz | |
| Profinite.empty_is_initial | |
| Profinite.epi_free'_to_condensed_setup.obj.add_comm_group | |
| Profinite.equalizer.lift | |
| Profinite.extend_unique | |
| Profinite.is_limit_arrow_cone | |
| Profinite.is_limit_prod_cone | |
| Profinite.normed_free_pfpng | |
| Profinite.normed_free_pfpng_level_iso | |
| Profinite.normed_free_pfpng_π | |
| Profinite.prod_cone | |
| Profinite.prod_iso | |
| Profinite.sigma_iso_empty | |
| Profinite.sigma_sum_iso | |
| Profinite.sum_iso_coprod | |
| Profinite.to_normed_free_pfpng | |
| pseudo_normed_group.filtration_prod_equiv | |
| pseudo_normed_group.pow_incl | |
| pseudo_normed_group.prod | |
| PseuNormGrp₁.category_theory.limits.has_limits | |
| PseuNormGrp₁.neg_nat_trans | |
| punit.profinitely_filtered_pseudo_normed_group | |
| punit.profinitely_filtered_pseudo_normed_group_with_Tinv | |
| rational.nnabs | |
| real_measures.metric.closed_ball.has_zero | |
| rel.decidable_rel | |
| rescale.add_comm_monoid | |
| SemiNormedGroup.normed_with_aut_Completion | |
| SemiNormedGroup.normed_with_aut_LCC | |
| short_complex.category_theory.limits.has_colimit | |
| short_complex.functor_category_equivalence | |
| short_complex.functor_category_equivalence.unit_iso | |
| short_complex.functor_category_equivalence.unit_iso.obj | |
| short_complex.homology_functor.category_theory.limits.preserves_colimits_of_shape | |
| short_complex.π₁_preserves_colimit | |
| short_complex.π₂_preserves_colimit | |
| short_complex.π₃_preserves_colimit | |
| sign_vectors_inhabited | |
| strict_comphaus_filtered_pseudo_normed_group_hom.inhabited | |
| sum_str.op | |
| sum_str.unop | |
| system_of_complexes.completion | |
| system_of_complexes.congr | |
| system_of_double_complexes.congr | |
| system_of_double_complexes.normed_spectral.one_le_K₀ | |
| tactic.extract_facts | |
| tactic.interactive.asyncI | |
| tactic.interactive.fact_arith | |
| tactic.prove_goal_asyncI | |
| theta.aux_y | |
| theta.y | |
| theta.ϑ' | |
| theta.ϑ₀ | |
| theta.ϑ_section | |
| thm95.col_complex_obj_iso_X_zero | |
| thm95.rescale_functor' | |
| thm95.rescale_functor'.additive | |
| thm95.rescale_nat_trans' | |
| thm95.scale' | |
| thm95.to_rescale' | |
| thm95.universal_constants.fact_κ'_le_k' | |
| thm95.universal_constants.K₀ | |
| thm95.universal_constants.one_le_K | |
| two_step_resolution | |
| two_step_resolution_ab | |
| two_step_resolution_ab_d | |
| two_step_resolution_ab_X | |
| two_step_resolution_d | |
| two_step_resolution_hom | |
| two_step_resolution_hom_ab | |
| two_step_resolution_X | |
| type_pow_topology.topological_space |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment