Theorem Real.one_add_inv_pow_le_exp

Modification history

2026-06-13 17:40
Mathlib/Analysis/Complex/Exponential.lean
feat(Analysis/Complex/Exponential): add new bounds on exponential (#39690) …
Added Real.one_add_inv_pow_le_expView on Github →