Theorem Complex.mul_cpow_of_le_neg_pi

Modification history

2026-11-10 22:59
Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
feat(Analysis/Complex): `(a * b) ^ r = a ^ r * b ^ r` (#45726) …
Added Complex.mul_cpow_of_le_neg_piView on Github →