cast_npow — Mathlib

English

Let R be a NonAssocSemiring with Pow by ℕ and NatPowAssoc. Then for all n,m ∈ ℕ, (↑(n^m) : R) = (↑n : R)^m.

Русский

Пусть R — неассоциированная полугруппа полукольца с мощностью по ℕ и NatPowAssoc. Тогда для всех n,m ∈ ℕ выполняется (↑(n^m) : R) = (↑n : R)^m.

LaTeX

$$$ (\uparrow(n^m) : R) = (\uparrow n : R)^m $$$

Lean4

@[simp, norm_cast]
theorem cast_npow (R : Type*) [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] (n m : ℕ) :
    (↑(n ^ m) : R) = (↑n : R) ^ m := by
  induction m with
  | zero => simp only [pow_zero, Nat.cast_one, npow_zero]
  | succ m ih => rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]

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