Commit 2024-07-27 08:25 743021e7

View on Github →

chore: robustifying for debug.byAsSorry (part 12) (#15178)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/GroupTheory/FixedPointFree.lean

modified theorem MonoidHom.FixedPointFree.coe_eq_inv_of_involutive

modified theorem MonoidHom.FixedPointFree.coe_eq_inv_of_sq_eq_one

modified def MonoidHom.FixedPointFree.commGroupOfInvolutive

modified theorem MonoidHom.FixedPointFree.commutatorMap_injective

modified theorem MonoidHom.FixedPointFree.commutatorMap_surjective

modified theorem MonoidHom.FixedPointFree.commute_all_of_involutive

modified theorem MonoidHom.FixedPointFree.odd_card_of_involutive

modified theorem MonoidHom.FixedPointFree.odd_orderOf_of_involutive

modified theorem MonoidHom.FixedPointFree.orderOf_ne_two_of_involutive

modified theorem MonoidHom.FixedPointFree.prod_pow_eq_one

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

modified theorem MonoidHom.independent_range_of_coprime_order

modified theorem MonoidHom.noncommPiCoprod_range

modified theorem Subgroup.commute_subtype_of_commute

modified theorem Subgroup.independent_of_coprime_order

modified theorem Subgroup.injective_noncommPiCoprod_of_independent

modified def Subgroup.noncommPiCoprod

modified theorem Subgroup.noncommPiCoprod_mulSingle

modified theorem Subgroup.noncommPiCoprod_range

Modified Mathlib/Order/WellFounded.lean

modified theorem WellFounded.eq_strictMono_iff_eq_range

modified theorem WellFounded.min_le

modified theorem WellFounded.self_le_of_strictMono

Modified Mathlib/RingTheory/Localization/Ideal.lean

modified theorem IsLocalization.map_comap

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Ordinal.lift_isLimit

Modified Mathlib/Topology/Algebra/Module/Star.lean