isometryEquivBasisRepr — Mathlib

English

A quadratic form is isometrically equivalent to its representation in a basis.

Русский

Квадратичная форма изометрически эквивалентна своему представлению в базисе.

LaTeX

$$$Q \;\text{is isometric to } Q_{\text{basisRepr}(v)}$ for a finite basis $v$.$$

Lean4

/-- A quadratic form is isometrically equivalent to its bases representations. -/
noncomputable def isometryEquivBasisRepr (Q : QuadraticMap R M N) (v : Basis ι R M) : IsometryEquiv Q (Q.basisRepr v) :=
  isometryEquivOfCompLinearEquiv Q v.equivFun.symm

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