Theorems · Definition · number theory

sigPos

{R : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommGroup M] → [inst_1 : CommRing R] → [LinearOrder R] → [inst_3 : Module R M] → QuadraticForm R M → ℕ

For quadratic forms on finite-dimensional spaces, the maximal finrank of a positive-definite subspace of M. (Defined as 0 if M is infinite-dimensional).

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Signature

Cited by

12 results in Mathlib

Foundations

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

Assumes

AddCommGroupCommRingLinearOrderModule