decomposeAux_eq_decompose — Mathlib

English

The auxiliary decomposition map decomposeAux f is identical to the canonical direct-sum decomposition map for the grading by gradeBy R f.

Русский

Дополнительная карта разложения decomposeAux f совпадает с каноническим отображением разложения по прямому сумме для градации gradeBy R f.

LaTeX

$$$decomposeAux\ f = DirectSum.decompose(\mathrm{gradeBy}\;R\;f)$$$

Lean4

@[simp]
theorem decomposeAux_eq_decompose :
    ⇑(decomposeAux f : R[M] →ₐ[R] ⨁ i : ι, gradeBy R f i) = DirectSum.decompose (gradeBy R f) :=
  rfl

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