coord_self — Mathlib

English

For any nonzero x ∈ E, coord 𝕜 x h acting on the vector x (viewed as a span) yields 1.

Русский

Для ненулевого x ∈ E операция coord 𝕜 x h, применённая к вектору x (воспринимаемому как множитель в span), даёт 1.

LaTeX

$$$ coord\\, 𝕜\\, x\\, h (\\langle x, \\text{mem\_span\_singleton\_self }\\, x\\rangle : 𝕜\\cdot x) = 1 $$$

Lean4

@[simp]
theorem coord_self (x : E) (h : x ≠ 0) : (coord 𝕜 x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : 𝕜 ∙ x) = 1 :=
  LinearEquiv.coord_self 𝕜 E x h

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