Theorem ofLex_smul

Modification history

2022-12-02 17:02

Mathlib/Algebra/Group/OrderSynonym.lean

feat: to_additive can reorder arguments of generated declaration (#818) …

Deleted ofLex_smul View on Github →

2022-11-23 13:35

Mathlib/Algebra/Group/OrderSynonym.lean

feat(Algebra.Group.Defs): add IsCancelMul (#606) …

Modified ofLex_smul View on Github →

2022-11-20 20:44

Mathlib/Algebra/Group/OrderSynonym.lean

feat: port Algebra.Group.OrderSynonym (#651) …

Added ofLex_smul View on Github →