toDirectSum_pow — Mathlib

English

Powers are preserved under the isomorphism to DirectSum: the image of f^n in DirectSum equals the DirectSum image of f raised to n.

Русский

Степени сохраняются при переходе через изоморфизм к DirectSum: образ f^n в DirectSum равен образу f в DirectSum, вознесенному в степень n.

LaTeX

$$$ (f^n).toDirectSum = f.toDirectSum^n $$$

Lean4

@[simp]
theorem toDirectSum_pow [DecidableEq ι] [AddMonoid ι] [Semiring M] (f : AddMonoidAlgebra M ι) (n : ℕ) :
    (f ^ n).toDirectSum = f.toDirectSum ^ n := by classical exact map_pow addMonoidAlgebraRingEquivDirectSum f n

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