Theorem le_iff_forall_one_lt_le_mul

Modification history

2024-11-18 18:16
Mathlib/Algebra/Order/Group/DenselyOrdered.lean
feat(Mathlib/Algebra/Order): add equivalent conditions to `a ≤ b` (#19166) …
Modified le_iff_forall_one_lt_le_mulView on Github →
2022-12-12 09:20
Mathlib/Algebra/Order/Group/DenselyOrdered.lean
feat: port algebra.order.group.densely_ordered (#956) …
Added le_iff_forall_one_lt_le_mulView on Github →