Theorems · Definition · number theory

QuadraticForm.isometryEquivSumSquaresUnits

{ι : Type u_1} →
  [inst : Fintype ι] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [IsAlgClosed K] →
          [DecidableEq K] →
            (w : ι → Kˣ) → (QuadraticMap.weightedSumSquares K w).IsometryEquiv (QuadraticMap.weightedSumSquares K 1)

The isometry between a weighted sum of squares on an algebraically closed field and the sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFieldIsAlgClosedDecidableEq