innerₗ — Mathlib

English

A linear equivalence preserving inner product yields a linear isometric equivalence.

Русский

Линейная эквиваленция, сохраняющая скалярное произведение, даёт линейную изометрию-эквиваленцию.

LaTeX

$$$ f: E \\simeq_ℓ[𝕜] E' \\text{ with inner preservation } \\Rightarrow f \\text{ is a linear isometry }$$$

Lean4

/-- The inner product as a bilinear map in the real case. -/
def innerₗ : F →ₗ[ℝ] F →ₗ[ℝ] ℝ :=
  innerₛₗ ℝ

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