lsum_single — Mathlib

English

Two linear maps f and g from the product to M are equal iff they agree on all pure coordinate injections Pi.single i x.

Русский

Линейные отображения f и g из произведения в M равны тогда и только тогда, когда они согласуются на всех координатных инъекциях Pi.single i x.

LaTeX

$$$f = g \\iff \\forall i x, f(\\Pi.single i x) = g(\\Pi.single i x).$$$

Lean4

@[simp high]
theorem lsum_single (S) [Fintype ι] [Semiring S] [∀ i, Module S (φ i)] [∀ i, SMulCommClass R S (φ i)] :
    LinearMap.lsum R φ S (LinearMap.single R φ) = LinearMap.id :=
  LinearMap.ext fun x => by simp [Finset.univ_sum_single]

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