Commit 2025-11-14 17:31 108a53e8

View on Github →

feat(Algebra/Homology): sandwich a comm group between two finite comm groups (#31227) From ClassFieldTheory

Estimated changes

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

added theorem CategoryTheory.ShortComplex.Exact.ab_finite

deleted theorem CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact

added theorem CategoryTheory.ShortComplex.ShortExact.ab_finite_iff

Modified Mathlib/Data/Finite/Prod.lean

added theorem Prod.finite_iff

Modified Mathlib/Data/Set/Finite/Basic.lean

added theorem Set.finite_range_iff

modified theorem Set.infinite_range_iff

Modified Mathlib/GroupTheory/QuotientGroup/Finite.lean

deleted theorem Finite.of_finite_quot_finite_subgroup

added theorem Finite.of_subgroup_quotient

added theorem finite_iff_subgroup_quotient

Modified Mathlib/RingTheory/Ideal/Quotient/Basic.lean

deleted theorem Finite.of_finite_quot_finite_ideal

added theorem Ideal.Quotient.Finite.of_ideal_quotient

added theorem Ideal.Quotient.finite_iff_ideal_quotient

added theorem Ideal.Quotient.map_pi

modified theorem Ideal.Quotient.mk_span_range

added theorem Ideal.Quotient.univ_eq_iUnion_image_add

deleted theorem Ideal.map_pi

deleted theorem Ideal.univ_eq_iUnion_image_add

Modified Mathlib/Topology/Algebra/Valued/LocallyCompact.lean