cpow_int_mul — Mathlib

English

For all x ∈ ℂ, integers n ∈ ℤ, y ∈ ℂ, x^(n y) = (x^y)^n.

Русский

Для всех x ∈ ℂ, целые n ∈ ℤ, y ∈ ℂ: x^(n y) = (x^y)^n.

LaTeX

$$$$ x^{(n \cdot y)} = (x^{y})^{n} \quad (n \in \mathbb{Z},\ y \in \mathbb{C}). $$$$

Lean4

/-- See also `Complex.cpow_int_mul'`. -/
theorem cpow_int_mul (x : ℂ) (n : ℤ) (y : ℂ) : x ^ (n * y) = (x ^ y) ^ n :=
  by
  rcases eq_or_ne x 0 with rfl | hx
  · rcases eq_or_ne n 0 with rfl | hn
    · simp
    · rcases eq_or_ne y 0 with rfl | hy <;> simp [*, zero_zpow]
  · rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]

Похожие утверждения