natCast_cpow_natCast_mul — Mathlib

English

For n,m ∈ ℕ and z ∈ ℂ, (n : ℂ)^(m·z) = ((n : ℂ)^m)^z.

Русский

Для n,m ∈ ℕ и z ∈ ℂ верно (n : ℂ)^(m·z) = ((n : ℂ)^m)^z.

LaTeX

$$$(n : \mathbb{C})^{(m \cdot z)} = ((n : \mathbb{C})^{m})^{z}$$$

Lean4

theorem natCast_cpow_natCast_mul (n m : ℕ) (z : ℂ) : (n : ℂ) ^ (m * z) = ((n : ℂ) ^ m) ^ z :=
  by
  refine cpow_nat_mul' (x := n) (n := m) ?_ ?_ z
  · simp only [natCast_arg, mul_zero, Left.neg_neg_iff, pi_pos]
  · simp only [natCast_arg, mul_zero, pi_pos.le]

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