English
A general variant: a map f preserves the inner form if and only if it preserves the norm for all vectors; equivalently, inner products are preserved.
Русский
Обобщённый вариант: отображение f сохраняет форму скалярного произведения тогда, когда сохраняет норму каждого вектора; эквивалентно сохранению скалярного произведения.
LaTeX
$$$( \\forall x:\\ E, \\|f x\\| = \\|x\\|) \\iff ( \\forall x,y:\\ E, \\langle f x, f y \\rangle = \\langle x, y \\rangle)$$$
Lean4
/-- The inner product as a sesquilinear map. -/
def innerₛₗ : E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜 :=
LinearMap.mk₂'ₛₗ _ _ (fun v w => ⟪v, w⟫) inner_add_left (fun _ _ _ => inner_smul_left _ _ _) inner_add_right
fun _ _ _ => inner_smul_right _ _ _
