Theorem le_of_forall_one_lt_div_le

Modification history

2022-12-12 09:20
Mathlib/Algebra/Order/Group/DenselyOrdered.lean
feat: port algebra.order.group.densely_ordered (#956) …
Added le_of_forall_one_lt_div_leView on Github →