cast_pow — Mathlib

English

Casting commutes with natural power: the cast of m^n equals (m^α)^n where m^α is the cast of m.

Русский

Преобразование Нат к α сохраняет возведение в натуральную степень: (m^n)^{\alpha} = (m^{\alpha})^n.

LaTeX

$$$ (m^{n})^{\alpha} = (m^{\alpha})^{n} $$$

Lean4

@[simp, norm_cast]
theorem cast_pow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n) = (m ^ n : α)
  | 0 => by simp
  | n + 1 => by rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]

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