toSpanUnitSingleton_apply — Mathlib

English

For a unit vector x with ∥x∥ = 1, the map toSpanUnitSingleton 𝕜 x hx sends r ∈ 𝕜 to r x.

Русский

Для единичного вектора x с ∥x∥ = 1 отображение toSpanUnitSingleton 𝕜 x hx отправляет r ∈ 𝕜 в r x.

LaTeX

$$$ toSpanUnitSingleton\\, x\\, hx\\, r = (r\\cdot x) $$$

Lean4

@[simp]
theorem toSpanUnitSingleton_apply (x : E) (hx : ‖x‖ = 1) (r : 𝕜) :
    toSpanUnitSingleton x hx r = (⟨r • x, by aesop⟩ : 𝕜 ∙ x) := by rfl

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