Theorem half_lt_self_iff

Modification history

2023-04-29 16:26
Mathlib/Algebra/Order/Field/Basic.lean
feat: `a * b ≠ b ↔ a ≠ 1` (#3726) …
Added half_lt_self_iffView on Github →