Theorem Real.mul_add_one_le_add_one_pow

Modification history

2024-08-04 14:32
Mathlib/Data/Real/Basic.lean
feat: Real.exists_natCast_add_one_le_pow_of_one_le (#15074) …
Added Real.mul_add_one_le_add_one_powView on Github →