Theorem Multiplicative.ofAdd_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 Multiplicative.ofAdd_lt View on Github →

2022-12-07 03:37

Mathlib/Algebra/Order/Monoid/TypeTags.lean

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

Added Multiplicative.ofAdd_lt View on Github →