Theorem Complex.norm_exp_I_mul_ofReal_sub_one

Modification history

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