Theorems · Definition · number theory
QuadraticMap.PosDef
{M : Type u_4} →
{N : Type u_5} →
{R₂ : Type u} →
[inst : CommSemiring R₂] →
[inst_1 : AddCommMonoid M] →
[inst_2 : Module R₂ M] →
[PartialOrder N] → [inst_4 : AddCommMonoid N] → [inst_5 : Module R₂ N] → QuadraticMap R₂ M N → PropA positive definite quadratic form is positive on nonzero vectors.
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 38 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- PartialOrderstatement and proof · cited by 6,410
- QuadraticMapstatement and proof · cited by 262
Cited by32
Results whose statement or proof uses this declaration.
- sigPosproof · cited by 12
- sigPos_isGreateststatement and proof · cited by 4
- QuadraticMap.Equivalent.sigPos_eqproof · cited by 3
- QuadraticMap.PosDef.anisotropicstatement and proof · cited by 2
- QuadraticMap.PosDef.nonnegstatement and proof · cited by 2
- RootPairing.posRootForm_rootFormIn_posDefstatement · cited by 2
- exists_finrank_eq_sigPos_and_posDefstatement · cited by 2
- QuadraticMap.PosDef.le_zero_iffstatement and proof · cited by 1
- le_sigPos_of_posDefstatement and proof · cited by 1
- QuadraticMap.posDef_of_nonnegstatement · cited by 1
- QuadraticMap.posDef_prod_iffstatement · cited by 1
- LinearMap.BilinForm.linearIndependent_of_pairwise_le_zerostatement and proof · cited by 1