toSpanNonzeroSingleton_coord — Mathlib

English

For x ≠ 0 and y in span{x}, applying the span map to coord 𝕜 x h y returns y.

Русский

Пусть x ≠ 0 и y ∈ span{x}. Применение отображения span к coord 𝕜 x h y возвращает y.

LaTeX

$$$ toSpanNonzeroSingleton\\, 𝕜\\, x\\, h (coord\\, 𝕜\\, x\\, h\\, y) = y $$$

Lean4

@[simp]
theorem toSpanNonzeroSingleton_coord {x : E} (h : x ≠ 0) (y : 𝕜 ∙ x) :
    toSpanNonzeroSingleton 𝕜 x h (coord 𝕜 x h y) = y :=
  (toSpanNonzeroSingleton 𝕜 x h).apply_symm_apply y

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