coeLinearMap_eq_dfinsuppSum — Mathlib

English

Same as above: if p ∈ weightedHomogeneousSubmodule R w n, then weightedHomogeneousComponent w m p equals p if m = n, else 0.

Русский

То же самое: если p ∈ weightedHomogeneousSubmodule R w n, тогда weightedHomogeneousComponent w m p = p при m = n, иначе 0.

LaTeX

$$$p ∈ weightedHomogeneousSubmodule\, R\, w\, n \Rightarrow weightedHomogeneousComponent\, w\, m\, p = \begin{cases} p, & m = n \\ 0, & m ≠ n \end{cases}$$$

Lean4

theorem coeLinearMap_eq_dfinsuppSum [DecidableEq σ] [DecidableEq R] [DecidableEq M]
    (x : DirectSum M fun i : M => ↥(weightedHomogeneousSubmodule R w i)) :
    (coeLinearMap fun i : M => weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x (fun _ x => ↑x) := by
  rw [_root_.DirectSum.coeLinearMap_eq_dfinsuppSum]

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