Commit 2024-07-30 13:32 df2eea5e

View on Github →

chore: backports for leanprover/lean4#4814 (part 5) (#15310) See https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

Modified Mathlib/Algebra/Group/Support.lean

modified theorem Function.mulSupport_extend_one

modified theorem Function.mulSupport_extend_one_subset

Modified Mathlib/Algebra/Module/Defs.lean

modified theorem Nat.noZeroSMulDivisors

modified theorem NoZeroSMulDivisors.int_of_charZero

modified theorem neg_eq_self

modified theorem neg_ne_self

modified theorem self_eq_neg

modified theorem self_ne_neg

modified theorem two_nsmul_eq_zero

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

modified theorem CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right

modified theorem CategoryTheory.Adjunction.isEquivalence_right_of_isEquivalence_left

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

modified theorem CategoryTheory.AreEqualizedByLocalization.map_eq

modified theorem CategoryTheory.Localization.Lifting.compLeft_iso

modified theorem CategoryTheory.Localization.faithful_whiskeringLeft

modified theorem CategoryTheory.Localization.full_whiskeringLeft

modified theorem CategoryTheory.Localization.natTrans_ext

modified def CategoryTheory.Localization.whiskeringLeftFunctor'

Modified Mathlib/Order/Booleanisation.lean

Modified Mathlib/Order/Monotone/Basic.lean