coord_toSpanNonzeroSingleton — Mathlib

English

For x ≠ 0 and c ∈ 𝕜, coord 𝕜 x h (toSpanNonzeroSingleton 𝕜 x h c) = c.

Русский

Пусть x ≠ 0 и c ∈ 𝕜. coord 𝕜 x h (toSpanNonzeroSingleton 𝕜 x h c) = c.

LaTeX

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

Lean4

@[simp]
theorem coord_toSpanNonzeroSingleton {x : E} (h : x ≠ 0) (c : 𝕜) : coord 𝕜 x h (toSpanNonzeroSingleton 𝕜 x h c) = c :=
  (toSpanNonzeroSingleton 𝕜 x h).symm_apply_apply c

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