Isometries with respect to quadratic forms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
Main results #
An isometry between two quadratic spaces
M₁, Q₁ and
M₂, Q₂ over a ring
is a linear equivalence between
M₂ that commutes with the quadratic forms.
Two quadratic forms over a ring
R are equivalent
if there exists an isometry between them:
a linear equivalence that transforms one quadratic form into the other.
The identity isometry from a quadratic form to itself.
The inverse isometry of an isometry between two quadratic forms.
The composition of two isometries between quadratic forms.
A quadratic form composed with a
linear_equiv is isometric to itself.
A quadratic form is isometric to its bases representations.
Given an orthogonal basis, a quadratic form is isometric with a weighted sum of squares.