Main results 1 to 100

Declaration Kind Where Note
CategoryTheory.isNoetherianObject_biprod instance HomologicalAlgebra/Abelian/ChainConditions.lean, line 38
CategoryTheory.isArtinianObject_biprod instance HomologicalAlgebra/Abelian/ChainConditions.lean, line 46
CategoryTheory.Limits.biprod.isIso_map_iff theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 54
CategoryTheory.Limits.biprod.mapIso_asIso theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 108
CategoryTheory.End.biprod_inl_comp_snd_eq_zero theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 127
CategoryTheory.End.biprod_inr_comp_fst_eq_zero theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 142
CategoryTheory.End.biprod_intertwiner_eq_map theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 158
CategoryTheory.End.biprodLeftIso def HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 180
CategoryTheory.End.biprodRightIso def HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 199
CategoryTheory.End.biprodLeftIso_hom theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 218
CategoryTheory.End.biprodLeftIso_inv theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 255
CategoryTheory.End.biprodRightIso_hom theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 230
CategoryTheory.End.biprodRightIso_inv theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 272
CategoryTheory.End.biprod_mapIso_eq_asIso theorem HomologicalAlgebra/Abelian/BiproductIntertwiners.lean, line 241
CategoryTheory.End.eq_zero_of_isNilpotent_of_mono theorem HomologicalAlgebra/Abelian/EndomorphismPowers.lean, line 104
CategoryTheory.End.eq_zero_of_epi_of_isNilpotent theorem HomologicalAlgebra/Abelian/EndomorphismPowers.lean, line 114
CategoryTheory.End.pow_biprod_desc_naturality theorem HomologicalAlgebra/Abelian/EndomorphismPowers.lean, line 126
CategoryTheory.End.comp_pow_succ theorem HomologicalAlgebra/Abelian/EndomorphismCyclicProducts.lean, line 41
CategoryTheory.End.comp_pow_comp_eq_mul_pow_mul theorem HomologicalAlgebra/Abelian/EndomorphismCyclicProducts.lean, line 52
CategoryTheory.End.isNilpotent_comp_iff theorem HomologicalAlgebra/Abelian/EndomorphismCyclicProducts.lean, line 60
CategoryTheory.End.eventually_exists_pow_biprod_desc_iso_naturality theorem HomologicalAlgebra/Abelian/FittingNaturality.lean, line 50
CategoryTheory.End.drazinInverse def HomologicalAlgebra/Abelian/Drazin.lean, line 203
CategoryTheory.End.commute_drazinInverse theorem HomologicalAlgebra/Abelian/Drazin.lean, line 216
CategoryTheory.End.drazinInverse_mul_self_mul theorem HomologicalAlgebra/Abelian/Drazin.lean, line 221
CategoryTheory.End.drazinInverse_comp_self_comp theorem HomologicalAlgebra/Abelian/Drazin.lean, line 228
CategoryTheory.End.exists_pow_succ_mul_drazinInverse theorem HomologicalAlgebra/Abelian/Drazin.lean, line 235
CategoryTheory.End.eq_drazinInverse_iff theorem HomologicalAlgebra/Abelian/Drazin.lean, line 242
CategoryTheory.End.existsUnique_drazinInverse theorem HomologicalAlgebra/Abelian/Drazin.lean, line 258
CategoryTheory.End.drazinInverse_eq_zero_iff theorem HomologicalAlgebra/Abelian/Drazin.lean, line 269
CategoryTheory.End.drazinInverse_zero theorem HomologicalAlgebra/Abelian/Drazin.lean, line 286
CategoryTheory.End.drazinInverse_eq_inv theorem HomologicalAlgebra/Abelian/Drazin.lean, line 291
CategoryTheory.End.drazinInverse_of_isIdempotentElem theorem HomologicalAlgebra/Abelian/Drazin.lean, line 305
CategoryTheory.End.isIdempotentElem_mul_drazinInverse theorem HomologicalAlgebra/Abelian/Drazin.lean, line 314
CategoryTheory.End.map_drazinInverse theorem HomologicalAlgebra/Abelian/Drazin.lean, line 479
CategoryTheory.Functor.map_drazinInverse theorem HomologicalAlgebra/Abelian/Drazin.lean, line 513
CategoryTheory.End.drazinInverse_comp_eq_comp_drazinInverse theorem HomologicalAlgebra/Abelian/Drazin.lean, line 325
Commute.drazinInverse_left theorem HomologicalAlgebra/Abelian/Drazin.lean, line 378
CategoryTheory.End.drazinInverse_pow theorem HomologicalAlgebra/Abelian/Drazin.lean, line 388
Commute.drazinInverse_mul theorem HomologicalAlgebra/Abelian/Drazin.lean, line 411
CategoryTheory.End.drazinInverse_drazinInverse theorem HomologicalAlgebra/Abelian/Drazin.lean, line 451
CategoryTheory.End.drazinInverse_add_of_mul_eq_zero theorem HomologicalAlgebra/Abelian/DrazinAdditivity.lean, line 49
CategoryTheory.End.drazinInverse_sum theorem HomologicalAlgebra/Abelian/DrazinAdditivity.lean, line 132
CategoryTheory.End.drazinInverse_comp theorem HomologicalAlgebra/Abelian/DrazinCyclic.lean, line 57
CategoryTheory.End.mul_drazinInverse_comp theorem HomologicalAlgebra/Abelian/DrazinCyclic.lean, line 75
CategoryTheory.End.imageMulDrazinInverseCompIso def HomologicalAlgebra/Abelian/DrazinCyclic.lean, line 85
CategoryTheory.End.imageMulDrazinInverseCompIso_hom_ι theorem HomologicalAlgebra/Abelian/DrazinCyclic.lean, line 147
CategoryTheory.End.imageMulDrazinInverseCompIso_inv_ι theorem HomologicalAlgebra/Abelian/DrazinCyclic.lean, line 155
CategoryTheory.End.imageMulDrazinInverseCompIso_hom_eq_image_map theorem HomologicalAlgebra/Abelian/DrazinCyclic.lean, line 164
CategoryTheory.End.imageMulDrazinInverseCompIso_inv_eq_image_map theorem HomologicalAlgebra/Abelian/DrazinCyclic.lean, line 179
CategoryTheory.End.imageMulDrazinInverseCompIso_hom_naturality theorem HomologicalAlgebra/Abelian/DrazinCyclic.lean, line 201
CategoryTheory.End.eventually_kernelSubobject_pow_eq_mul_drazinInverse theorem HomologicalAlgebra/Abelian/DrazinProjector.lean, line 72
CategoryTheory.End.eventually_imageSubobject_pow_eq_mul_drazinInverse theorem HomologicalAlgebra/Abelian/DrazinProjector.lean, line 85
CategoryTheory.End.isNilpotent_mul_one_sub_mul_drazinInverse theorem HomologicalAlgebra/Abelian/DrazinProjector.lean, line 98
CategoryTheory.End.drazinInverse_add_eq_sum_range theorem HomologicalAlgebra/Abelian/DrazinPerturbation.lean, line 165
CategoryTheory.End.add_mul_drazinInverse_of_isNilpotent theorem HomologicalAlgebra/Abelian/DrazinPerturbation.lean, line 196
CategoryTheory.existsUnique_sylvester theorem HomologicalAlgebra/Preadditive/Sylvester.lean, line 37
CategoryTheory.End.eq_comp_inl_drazinInverse_biprod_triangular_snd_iff theorem HomologicalAlgebra/Abelian/DrazinTriangular.lean, line 277
CategoryTheory.End.eq_imageMulDrazinInverseBiprodTriangularIso_inv_ι_iff theorem HomologicalAlgebra/Abelian/DrazinTriangular.lean, line 322
CategoryTheory.End.drazinInverse_biprod_triangular theorem HomologicalAlgebra/Abelian/DrazinTriangular.lean, line 74
CategoryTheory.End.mul_drazinInverse_biprod_triangular theorem HomologicalAlgebra/Abelian/DrazinTriangular.lean, line 140
CategoryTheory.End.imageMulDrazinInverseBiprodTriangularIso def HomologicalAlgebra/Abelian/DrazinTriangular.lean, line 183
CategoryTheory.End.imageMulDrazinInverseBiprodTriangularIso_hom theorem HomologicalAlgebra/Abelian/DrazinTriangular.lean, line 211
CategoryTheory.End.imageMulDrazinInverseBiprodTriangularIso_inv_ι theorem HomologicalAlgebra/Abelian/DrazinTriangular.lean, line 241
CategoryTheory.End.factorThruImage_comp_imageMulDrazinInverseBiprodTriangularIso_hom theorem HomologicalAlgebra/Abelian/DrazinTriangular.lean, line 261
CategoryTheory.cancel_finite_biproduct_of_isLocalRing_end theorem HomologicalAlgebra/Preadditive/FiniteCancellation.lean, line 106
CategoryTheory.nonempty_iso_of_biprod_iso_of_isNoetherianObject_of_isArtinianObject theorem HomologicalAlgebra/Abelian/FiniteLengthCancellation.lean, line 46
CategoryTheory.exists_finite_biproduct_isLocalRing_end theorem HomologicalAlgebra/Abelian/FiniteLength.lean, line 48
CategoryTheory.exists_equiv_of_iso_biproduct_of_isLocalRing_end theorem HomologicalAlgebra/Preadditive/BiproductUniqueness.lean, line 223
CategoryTheory.exists_finite_indecomposable_biproduct_of_isArtinianObject theorem HomologicalAlgebra/Indecomposable/Artinian.lean, line 39
CategoryTheory.exists_finite_indecomposable_biproduct_of_isNoetherianObject theorem HomologicalAlgebra/Indecomposable/Noetherian.lean, line 192
CategoryTheory.indecomposable_of_isLocalRing_end theorem HomologicalAlgebra/Preadditive/Indecomposable.lean, line 45
CategoryTheory.isLocalRing_end_of_indecomposable theorem HomologicalAlgebra/Abelian/LocalEndomorphism.lean, line 73
CategoryTheory.isNilpotent_or_isUnit_of_indecomposable theorem HomologicalAlgebra/Abelian/LocalEndomorphism.lean, line 50
ModuleCat.isArtinianObject_iff lemma HomologicalAlgebra/ModuleCat/Subobject.lean, line 36
CategoryTheory.eventually_isCompl_kernelSubobject_pow_imageSubobject_pow theorem HomologicalAlgebra/Abelian/Fitting.lean, line 245
CategoryTheory.eventually_isIso_biprod_desc_kernel_ι_image_ι_pow theorem HomologicalAlgebra/Abelian/Fitting.lean, line 255
CategoryTheory.End.eventually_isIso_imagePowRestriction theorem HomologicalAlgebra/Abelian/Fitting.lean, line 267
ModuleCat.isCompl_kernelSubobject_pow_imageSubobject_pow_iff lemma HomologicalAlgebra/ModuleCat/Subobject.lean, line 75
CochainComplex.HomComplex.isZero_homology_iff lemma HomologicalAlgebra/Cochain/HomComplexVanishing.lean, line 37
CochainComplex.HomComplex.acyclic_iff lemma HomologicalAlgebra/Cochain/HomComplexVanishing.lean, line 84
CochainComplex.HomComplex.quasiIso_prePostcomp_of_homotopyEquiv lemma HomologicalAlgebra/Cochain/HomComplexQuasiIso.lean, line 69
CochainComplex.HomComplex.quasiIso_prePostcomp_of_isIso_quotient_map lemma HomologicalAlgebra/Cochain/HomComplexQuasiIso.lean, line 107
CochainComplex.IsKProjective.quasiIso_prePostcomp lemma HomologicalAlgebra/Cochain/HomComplexQuasiIso.lean, line 134
CochainComplex.IsKInjective.quasiIso_prePostcomp lemma HomologicalAlgebra/Cochain/HomComplexQuasiIso.lean, line 208
CategoryTheory.ShortComplex.SnakeInput.composableArrowsWithEndpoints_middle_exact theorem HomologicalAlgebra/Abelian/SnakeLemma.lean, line 139
CategoryTheory.ShortComplex.SnakeInput.kernelToL₀X₁IsKernel def HomologicalAlgebra/Abelian/SnakeLemma.lean, line 57
CategoryTheory.ShortComplex.SnakeInput.L₃X₃ToCokernelIsCokernel def HomologicalAlgebra/Abelian/SnakeLemma.lean, line 94
CategoryTheory.ShortComplex.SnakeInput.snake_lemma_with_endpoints theorem HomologicalAlgebra/Abelian/SnakeLemma.lean, line 148
CategoryTheory.AdditiveEuler.euler_endpoints theorem HomologicalAlgebra/AdditiveEuler.lean, line 169
CategoryTheory.AdditiveEuler.euler_eq_homology_of_bounded theorem HomologicalAlgebra/AdditiveEuler.lean, line 205
CategoryTheory.AdditiveEuler.euler_quasiIso theorem HomologicalAlgebra/AdditiveEuler.lean, line 227
CategoryTheory.AdditiveEuler.lengthInvariant_ses theorem HomologicalAlgebra/AdditiveEuler/Length.lean, line 39
CategoryTheory.AdditiveEuler.term_sum_additive_of_shortExact theorem HomologicalAlgebra/AdditiveEuler/Functoriality.lean, line 39
CategoryTheory.AdditiveEuler.homology_sum_additive_of_shortExact theorem HomologicalAlgebra/AdditiveEuler/Functoriality.lean, line 53
CategoryTheory.AdditiveEuler.mapHomologyIso def HomologicalAlgebra/AdditiveEuler/Functoriality.lean, line 99
CategoryTheory.AdditiveEuler.euler_map_bounded theorem HomologicalAlgebra/AdditiveEuler/Functoriality.lean, line 132
CategoryTheory.AdditiveEuler.signed_sum_eq_of_support theorem HomologicalAlgebra/AdditiveEuler/Shift.lean, line 35
CategoryTheory.AdditiveEuler.signed_sum_translate theorem HomologicalAlgebra/AdditiveEuler/Shift.lean, line 55
CategoryTheory.AdditiveEuler.term_sum_eq_of_support theorem HomologicalAlgebra/AdditiveEuler/Shift.lean, line 87
CategoryTheory.AdditiveEuler.cochain_shift_term_support theorem HomologicalAlgebra/AdditiveEuler/Shift.lean, line 101

Quoted from the main results in formalization.yaml of FormalFrontier/homological-algebra at commit 8bcaebe9, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.