Theorem Complex.nnnorm_exp_ofReal_mul_I

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.nnnorm_exp_ofReal_mul_IView on Github →