Theorem one_sub_le_one_add_mul_one_sub

Modification history

2024-09-30 02:32
Mathlib/Algebra/Order/Ring/Defs.lean
feat: When `1 + a ≤ (1 - b) * (1 + c)` (#17214) …
Added one_sub_le_one_add_mul_one_subView on Github →