Theorem Complex.mul_cpow

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_cpowView on Github →