Theorems · Theorem · complex analysis
Complex.cpow_mul
∀ {x y : ℂ} (z : ℂ), -Real.pi < (Complex.log x * y).im → (Complex.log x * y).im ≤ Real.pi → x ^ (y * z) = (x ^ y) ^ z- Cited by
- 3 results in Mathlib
- Foundations
- Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement and proof · cited by 5,565
- MulZeroClass.mul_zeroproof · cited by 2,091
- Real.pistatement and proof · cited by 1,774
- mul_assocproof · cited by 1,667
- MulZeroClass.zero_mulproof · cited by 1,625
- Complex.expproof · cited by 612
- Complex.imstatement and proof · cited by 591
- Complex.logstatement and proof · cited by 187
- Complex.exp_zeroproof · cited by 43
- Complex.log_oneproof · cited by 7
- Complex.log_expproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- Real.rpow_mulproof · cited by 67
- Complex.cpow_mul_ofReal_nonnegproof · cited by 2
- Complex.cpow_int_mul'proof · cited by 1