Theorems · Theorem · number theory

QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed

∀ {K : Type u_2} [inst : Field K] [IsAlgClosed K] [inst_2 : Invertible 2] {M : Type u_3} [inst_3 : AddCommGroup M]
  [inst_4 : Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M),
  LinearMap.SeparatingLeft (QuadraticMap.associated Q) → QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K 1)

A nondegenerate quadratic form on an algebraically closed field of characteristic not equal to 2 is equivalent to the sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldIsAlgClosedInvertibleAddCommGroupModuleFiniteDimensional