Theorems · Theorem · number theory

QuadraticForm.sigNeg_weightedSumSquares

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

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Signature

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderFintypeIsStrictOrderedRing