Theorems · Theorem · number theory

QuadraticForm.sigPos_weightedSumSquares

∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {ι : Type u_5} [inst_2 : Fintype ι] {w : ι → 𝕜}
  [IsStrictOrderedRing 𝕜], sigPos (QuadraticMap.weightedSumSquares 𝕜 w) = {i | 0 < w i}.ncard

Key lemma for Sylvester's law of inertia: compute the signature of a weighted sum of squares.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Signature

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderFintypeIsStrictOrderedRing