Commit 2025-12-06 17:24 31ec2d9f

View on Github →

feat(Algebra/Homology): miscellaneous lemmas (#32434) From ClassFieldTheory

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/Exact.lean

added theorem CategoryTheory.ShortComplex.Exact.epi_kernelLift

added theorem CategoryTheory.ShortComplex.Exact.mono_cokernelDesc

Modified Mathlib/CategoryTheory/Abelian/Exact.lean

added theorem CategoryTheory.ShortComplex.Exact.isIso_imageToKernel'

added theorem CategoryTheory.ShortComplex.Exact.isIso_imageToKernel

added theorem CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel'