sumCoords — Mathlib

English

For a basis b of M, the sumCoords map is the linear functional that takes x ∈ M to the sum of its coordinates with respect to b; equivalently sumCoords(x) = ∑ i b.coord i x.

Русский

Для базиса b модуля M сумма координат представляет собой линейное отображение, отправляющее x ∈ M в сумму его координат по базису; то есть sumCoords(x) = ∑ i b.coord i x.

LaTeX

$$$\text{sumCoords} = (x \mapsto \sum_{i} b.coord\,i\, x)$$$$

Lean4

/-- The sum of the coordinates of an element `m : M` with respect to a basis. -/
noncomputable def sumCoords : M →ₗ[R] R :=
  (Finsupp.lsum ℕ fun _ => LinearMap.id) ∘ₗ (b.repr : M →ₗ[R] ι →₀ R)

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