Theorem sub_inv_antitoneOn_Icc_left

Modification history

2024-03-01 13:29
Mathlib/Algebra/Order/Field/Basic.lean
feat: explicit logarithmic bounds on the harmonic numbers (#9984) …
Added sub_inv_antitoneOn_Icc_leftView on Github →