Commit 2023-11-23 11:18 aa7a2917

View on Github →

chore(Algebra/Regular/Basic): generalize to IsCancelMul (#8428) This lets lemmas about cancellative monoids work for cancellative semigroups Some docstrings have been rewritten, as adjusting the wording was too awkward. The new .all names are intended to match Commute.all.

Estimated changes

Modified Mathlib/Algebra/CovariantAndContravariant.lean

Modified Mathlib/Algebra/Group/Embedding.lean

modified def mulLeftEmbedding

modified theorem mulLeftEmbedding_eq_mulRightEmbedding

modified def mulRightEmbedding

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

modified theorem AddMonoidAlgebra.support_mul_single

modified theorem AddMonoidAlgebra.support_single_mul

modified theorem MonoidAlgebra.support_mul_single

modified theorem MonoidAlgebra.support_single_mul

Modified Mathlib/Algebra/Order/Group/Defs.lean

Modified Mathlib/Algebra/Order/WithZero.lean

Modified Mathlib/Algebra/Regular/Basic.lean

added theorem IsLeftRegular.all

added theorem IsRegular.all

added theorem IsRightRegular.all

deleted theorem isLeftRegular_of_leftCancelSemigroup

deleted theorem isRegular_of_cancelMonoid

deleted theorem isRightRegular_of_rightCancelSemigroup

Modified Mathlib/Data/Finset/Pointwise.lean

Modified Mathlib/Data/Set/Pointwise/SMul.lean