coe_mkFinConsOfLE — Mathlib

English

The sumCoords map equals the finsum of the coordinate functionals: (b.sumCoords) = finsum i (b.coord i).

Русский

Сумма координат по базису равна финальной сумме координат: (b.sumCoords) = finsum i (b.coord i).

LaTeX

$$$ (b.sumCoords : M \to R) = \text{finsum}_{i} (b.coord i) $$$

Lean4

@[simp]
theorem coe_mkFinConsOfLE {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R N) (hNO : N ≤ O)
    (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ c : R, z + c • y ∈ N) :
    (mkFinConsOfLE y yO b hNO hli hsp : Fin (n + 1) → O) = Fin.cons ⟨y, yO⟩ (Submodule.inclusion hNO ∘ b) :=
  coe_mkFinCons _ _ _ _

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