decompose_single — Mathlib

English

The direct-sum decomposition of a simple basis element Finsupp.single m r lies in the i-th component determined by f(m).

Русский

Разложение простой базисной компоненты Finsupp.single m r лежит в компоненте, определяемой f(m).

LaTeX

$$$DirectSum.decompose(\mathrm{gradeBy}\;R\;f)(\mathsf{single}\,m\,r) = DirectSum.of(\lambda i. \mathrm{gradeBy}(R,f)_i)(f(m))\langle \mathsf{single}\,m\,r, \text{mem}_{{\mathrm{gradeBy}}}\rangle$$$

Lean4

theorem decompose_single (i : ι) (r : R) :
    DirectSum.decompose (grade R : ι → Submodule _ _) (Finsupp.single i r : AddMonoidAlgebra _ _) =
      DirectSum.of (fun i : ι => grade R i) i ⟨Finsupp.single i r, single_mem_grade _ _⟩ :=
  decomposeAux_single _ _ _

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