toSpanSingleton_apply — Mathlib

English

The toSpanSingleton_apply lemma states the equality for an isometry on a one-dimensional span.

Русский

Лемма toSpanSingleton_apply утверждает равенство для изометрии, действующей на единичном в_span.

LaTeX

$$$\text{LinearIsometry.toSpanSingleton } 𝕜 E hv a = a \cdot v$$$

Lean4

@[simp]
theorem _root_.LinearIsometry.toSpanSingleton_apply {v : E} (hv : ‖v‖ = 1) (a : 𝕜) :
    LinearIsometry.toSpanSingleton 𝕜 E hv a = a • v :=
  rfl

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