Theorems · Definition · number theory

QuadraticForm.isometryEquivWeightedSumSquares

{K : Type u_3} →
  {V : Type u_8} →
    [inst : Field K] →
      [inst_1 : Invertible 2] →
        [inst_2 : AddCommGroup V] →
          [inst_3 : Module K V] →
            (Q : QuadraticForm K V) →
              (v : Module.Basis (Fin (Module.finrank K V)) K V) →
                LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑v →
                  QuadraticMap.IsometryEquiv Q (QuadraticMap.weightedSumSquares K fun i => Q (v i))

Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of squares.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Cited by

2 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldInvertibleAddCommGroupModule