Theorem Additive.ofMul_lt

Modification history

2024-10-17 20:59

Mathlib/Algebra/Order/Monoid/TypeTags.lean

chore(Algebra.Order.Monoid.TypeTags): split into unbundled and bundled ordered algebra (#16047) …

Modified Additive.ofMul_lt View on Github →

2022-12-07 03:37

Mathlib/Algebra/Order/Monoid/TypeTags.lean

feat: port Algebra.Order.Monoid.[TypeTags, Units] (#873) …

Added Additive.ofMul_lt View on Github →