Commit 2024-07-31 03:44 c934de62

View on Github →

chore: backports for leanprover/lean4#4814 (part 9) (#15352) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

modified theorem ConjClasses.mem_noncenter

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

modified theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv

modified theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom

modified theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv

modified theorem CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv

modified theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv

modified theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_ι

modified theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_inv_comp_homologyι

modified theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv

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

Modified Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

Modified Mathlib/CategoryTheory/Limits/Elements.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

modified theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom

modified theorem CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι

modified theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift

modified theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom

Modified Mathlib/CategoryTheory/Limits/TypesFiltered.lean

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean

modified theorem CategoryTheory.MorphismProperty.LeftFraction₂Rel.fst

modified theorem CategoryTheory.MorphismProperty.LeftFraction₂Rel.snd

Modified Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

Modified Mathlib/CategoryTheory/Localization/Prod.lean

modified theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁

Modified Mathlib/CategoryTheory/Monad/Limits.lean

Modified Mathlib/CategoryTheory/SmallObject/Construction.lean

Modified Mathlib/Control/LawfulFix.lean

modified theorem Pi.uncurry_curry_continuous

Modified Mathlib/Control/Traversable/Instances.lean

modified theorem Option.naturality

Modified Mathlib/Data/Finset/Basic.lean

modified theorem Finset.Nonempty.exists_cons_eq

Modified Mathlib/Data/Finset/Lattice.lean

modified theorem Finset.nsmul_inf'

modified theorem Finset.nsmul_sup'

Modified Mathlib/Data/Set/Finite.lean

modified theorem Set.Finite.injOn_iff_bijOn_of_mapsTo

modified theorem Set.Finite.surjOn_iff_bijOn_of_mapsTo

Modified Mathlib/GroupTheory/GroupAction/Pointwise.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/Logic/Encodable/Basic.lean

modified theorem Encodable.decode_prod_val

Modified Mathlib/Order/Closure.lean

Modified Mathlib/Order/Grade.lean

modified theorem GradeOrder.wellFoundedGT

modified theorem GradeOrder.wellFoundedLT

modified theorem grade_mono

Modified Mathlib/Order/IsWellOrderLimitElement.lean

Modified Mathlib/Order/Minimal.lean

Modified Mathlib/Tactic/Ring/Basic.lean

modified theorem Mathlib.Tactic.Ring.of_eq