Theorem Complex.integrable_pow_mul_norm_one_add_mul_inv

Modification history

2024-01-07 18:13
Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
feat: estimates for the complex logarithm (#9270) …
Added Complex.integrable_pow_mul_norm_one_add_mul_invView on Github →