toDirectSum_comp_ofDirectSum — Mathlib

English

The composition of toDirectSum after ofDirectSum is the identity on the direct sum.

Русский

Составление toDirectSum после ofDirectSum дает тождество на прямой сумме.

LaTeX

$$$ toDirectSum.comp ofDirectSum = AlgHom.id R (⨁ n, ⨂[R]^n M) $$$

Lean4

theorem toDirectSum_comp_ofDirectSum : toDirectSum.comp ofDirectSum = AlgHom.id R (⨁ n, ⨂[R]^n M) :=
  by
  ext
  simp [DirectSum.lof_eq_of, -tprod_apply, toDirectSum_tensorPower_tprod]

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