ofFinsupp_pow — Mathlib

English

Let a ∈ AddMonoidAlgebra R Nat. For n ∈ ℕ, the finsupp embedding commutes with exponentiation: (⟨a^n⟩) = ⟨a⟩^n.

Русский

Пусть a ∈ AddMonoidAlgebra R Nat. Для n ∈ ℕ отображение in finsupp сохраняет возведение в степень: (⟨a^n⟩) = ⟨a⟩^n.

LaTeX

$$$\\langle a^n \\rangle = \\langle a \\rangle^n$$$

Lean4

@[simp]
theorem ofFinsupp_pow (a) (n : ℕ) : (⟨a ^ n⟩ : R[X]) = ⟨a⟩ ^ n :=
  by
  change _ = npowRec n _
  induction n with
  | zero => simp [npowRec]
  | succ n n_ih => simp [npowRec, n_ih, pow_succ]

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