Theorems · Theorem · number theory

exists_finrank_eq_sigPos_and_posDef

∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R],
  ∃ V, Module.finrank R ↥V = sigPos Q ∧ (QuadraticMap.restrict Q V).PosDef

Defined in: Mathlib.LinearAlgebra.QuadraticForm.Signature
Cited by: 2 results in Mathlib
Foundations: Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroup CommRing LinearOrder Module Module.Finite StrongRankCondition

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
LinearOrderstatement and proof · cited by 8,572
Submodulestatement · cited by 7,192
Module.finrankstatement · cited by 1,770
Module.Finitestatement and proof · cited by 1,032
QuadraticFormstatement and proof · cited by 507
StrongRankConditionstatement and proof · cited by 286
QuadraticMap.PosDefstatement · cited by 31
sigPosstatement · cited by 12
QuadraticMap.restrictstatement · cited by 12

Cited by2

Results whose statement or proof uses this declaration.

QuadraticForm.sigPos_add_finrank_le_of_nonposproof · cited by 1
exists_finrank_eq_sigNeg_and_negDefproof · cited by 0