Theorem Real.nnnorm_exp_I_mul_ofReal_sub_one_le

Modification history

2025-10-23 17:08
Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
feat: sharp bounds for `‖exp (I * x) - 1‖` when `x` is real (#27252) …
Added Real.nnnorm_exp_I_mul_ofReal_sub_one_leView on Github →