Commit 2022-11-23 13:35 a7cbedda

View on Github →

feat(Algebra.Group.Defs): add IsCancelMul (#606) We add a class IsCancelMul (and also other related classes). I've also fixed a lot of docstrings. Corresponding mathlib3 PR is [#17440](https://github.com/leanprover-community/mathlib/pull/17440).

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

added theorem CommSemigroup.IsLeftCancelMul.to_IsCancelMul

added theorem CommSemigroup.IsLeftCancelMul.to_IsRightCancelMul

added theorem CommSemigroup.IsRightCancelMul.to_IsCancelMul

added theorem CommSemigroup.IsRightCancelMul.to_IsLeftCancelMul

Modified Mathlib/Algebra/Group/OrderSynonym.lean

modified theorem ofDual_smul'

modified theorem ofDual_smul

modified theorem ofLex_smul'

modified theorem ofLex_smul

modified theorem toDual_smul'

modified theorem toDual_smul

modified theorem toLex_smul'

modified theorem toLex_smul

Modified Mathlib/Tactic/Abel.lean

Modified Mathlib/Tactic/Ring/Basic.lean

Modified scripts/nolints.json