coe_toSpanNonzeroSingleton_symm — Mathlib

English

For nonzero x, the symmetry (inverse) of the span map equals coord: (toSpanNonzeroSingleton 𝕜 x h).symm = coord 𝕜 x h.

Русский

Пусть x ≠ 0. Обратный отображение к отображению 𝕜 → 𝕜·x совпадает с coord: (toSpanNonzeroSingleton 𝕜 x h).symm = coord 𝕜 x h.

LaTeX

$$$ (toSpanNonzeroSingleton\\, 𝕜\\, x\\, h).symm = coord\\, 𝕜\\, x\\, h $$$

Lean4

@[simp]
theorem coe_toSpanNonzeroSingleton_symm {x : E} (h : x ≠ 0) : ⇑(toSpanNonzeroSingleton 𝕜 x h).symm = coord 𝕜 x h :=
  rfl

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