Theorem eq_one_or_one_lt

Modification history

2023-12-26 07:50

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

feat: `0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)` (#9219) …

Modified eq_one_or_one_lt View on Github →

2022-12-01 10:59

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

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

Added eq_one_or_one_lt View on Github →