toAddMonoidAlgebra_pow — Mathlib

English

Raising f to the power n commutes with the toAddMonoidAlgebra map: the image of f^n equals the n-th power of the image of f.

Русский

Возведение f в степень n коммутирует отображение в AddMonoidAlgebra: образ f^n равен n-й степени образа f.

LaTeX

$$$ (f^n).toAddMonoidAlgebra = (toAddMonoidAlgebra\, f)^n $$$

Lean4

@[simp]
theorem toAddMonoidAlgebra_pow [DecidableEq ι] [AddMonoid ι] [Semiring M] [∀ m : M, Decidable (m ≠ 0)] (f : ⨁ _ : ι, M)
    (n : ℕ) : (f ^ n).toAddMonoidAlgebra = toAddMonoidAlgebra f ^ n := by
  classical exact map_pow addMonoidAlgebraRingEquivDirectSum.symm f n

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