Theorem le_of_forall_lt_one_mul_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_lt_one_mul_leView on Github →