Theorem one_lt_mul_iff

Modification history

2022-12-01 10:59

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

feat: port Algebra.Order.Monoid.Canonical.Defs (#778) …

Added one_lt_mul_iff View on Github →