Quadratic form on product and pi types #
Main definitions #
QuadraticForm.prod Q₁ Q₂
: the quadratic form constructed elementwise on a productQuadraticForm.pi Q
: the quadratic form constructed elementwise on a pi type
Main results #
QuadraticForm.Equivalent.prod
,QuadraticForm.Equivalent.pi
: quadratic forms are equivalent if their components are equivalentQuadraticForm.nonneg_prod_iff
,QuadraticForm.nonneg_pi_iff
: quadratic forms are positive- semidefinite if and only if their components are positive-semidefinite.QuadraticForm.posDef_prod_iff
,QuadraticForm.posDef_pi_iff
: quadratic forms are positive- definite if and only if their components are positive-definite.
Implementation notes #
Many of the lemmas in this file could be generalized into results about sums of positive and
non-negative elements, and would generalize to any map Q
where Q 0 = 0
, not just quadratic
forms specifically.
Construct a quadratic form on a product of two modules from the quadratic form on each module.
Instances For
An isometry between quadratic forms generated by QuadraticForm.prod
can be constructed
from a pair of isometries between the left and right parts.
Instances For
LinearEquiv.prodComm
is isometric.
Instances For
LinearEquiv.prodProdProdComm
is isometric.
Instances For
If a product is anisotropic then its components must be. The converse is not true.
Construct a quadratic form on a family of modules from the quadratic form on each module.
Instances For
An isometry between quadratic forms generated by QuadraticForm.pi
can be constructed
from a pair of isometries between the left and right parts.
Instances For
If a family is anisotropic then its components must be. The converse is not true.