Commit 2025-07-18 23:34 0bab0826

View on Github →

feat(Algebra): MulOpposite lemmas (#27263) Also add more lemmas towards #27241:

generalize (Add)MonoidAlgebra.opRingEquiv to weaker typeclass assumptions.
add UniqueMul/Add.mono.
add stability of some typeclasses under MulEquivs.

Estimated changes

Modified Mathlib/Algebra/Group/Opposite.lean

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

added theorem UniqueMul.mono

Modified Mathlib/Algebra/GroupWithZero/Opposite.lean

added theorem MulOpposite.isCancelMulZero_iff

added theorem MulOpposite.isLeftCancelMulZero_iff

added theorem MulOpposite.isRightCancelMulZero_iff

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

modified theorem AddMonoidAlgebra.opRingEquiv_single

modified theorem AddMonoidAlgebra.opRingEquiv_symm_single

modified theorem MonoidAlgebra.opRingEquiv_single

modified theorem MonoidAlgebra.opRingEquiv_symm_single

Modified Mathlib/Algebra/Opposites.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

added theorem MulEquiv.isCancelMulZero_iff

added theorem MulEquiv.isDomain_iff

added theorem MulEquiv.isLeftCancelMulZero_iff

added theorem MulEquiv.isRightCancelMulZero_iff

added theorem MulEquiv.noZeroDivisors_iff