# Quadratic form on product and pi types #

## Main definitions #

• QuadraticForm.prod Q₁ Q₂: the quadratic form constructed elementwise on a product
• QuadraticForm.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 equivalent
• QuadraticForm.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.

@[simp]
theorem QuadraticMap.prod_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (a : M₁ × M₂) :
(Q₁.prod Q₂) a = Q₁ a.1 + Q₂ a.2
def QuadraticMap.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
QuadraticMap R (M₁ × M₂) P

Construct a quadratic form on a product of two modules from the quadratic form on each module.

Equations
Instances For
@[simp]
theorem QuadraticMap.IsometryEquiv.prod_toLinearEquiv {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [] [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P} {Q₂' : QuadraticMap R N₂ P} (e₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂') :
(e₁.prod e₂).toLinearEquiv = e₁.prod e₂.toLinearEquiv
def QuadraticMap.IsometryEquiv.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [] [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P} {Q₂' : QuadraticMap R N₂ P} (e₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂') :
(Q₁.prod Q₂).IsometryEquiv (Q₁'.prod Q₂')

An isometry between quadratic forms generated by QuadraticForm.prod can be constructed from a pair of isometries between the left and right parts.

Equations
• e₁.prod e₂ = { toLinearEquiv := e₁.prod e₂.toLinearEquiv, map_app' := }
Instances For
@[simp]
theorem QuadraticMap.Isometry.inl_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (i : M₁) :
() i = (i, 0)
def QuadraticMap.Isometry.inl {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
Q₁ →qᵢ Q₁.prod Q₂

LinearMap.inl as an isometry.

Equations
Instances For
@[simp]
theorem QuadraticMap.Isometry.inr_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (i : M₂) :
() i = (0, i)
def QuadraticMap.Isometry.inr {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
Q₂ →qᵢ Q₁.prod Q₂

LinearMap.inr as an isometry.

Equations
Instances For
@[simp]
theorem QuadraticMap.Isometry.fst_apply {R : Type u_2} {M₁ : Type u_3} (M₂ : Type u_4) {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (self : M₁ × M₂) :
() self = self.1
def QuadraticMap.Isometry.fst {R : Type u_2} {M₁ : Type u_3} (M₂ : Type u_4) {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) :
Q₁.prod 0 →qᵢ Q₁

LinearMap.fst as an isometry, when the second space has the zero quadratic form.

Equations
Instances For
@[simp]
theorem QuadraticMap.Isometry.snd_apply {R : Type u_2} (M₁ : Type u_3) {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₂ : QuadraticMap R M₂ P) (self : M₁ × M₂) :
() self = self.2
def QuadraticMap.Isometry.snd {R : Type u_2} (M₁ : Type u_3) {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₂ : QuadraticMap R M₂ P) :
→qᵢ Q₂

LinearMap.snd as an isometry, when the first space has the zero quadratic form.

Equations
Instances For
@[simp]
theorem QuadraticMap.Isometry.fst_comp_inl {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) :
().comp () =
@[simp]
theorem QuadraticMap.Isometry.snd_comp_inr {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₂ : QuadraticMap R M₂ P) :
().comp () =
@[simp]
theorem QuadraticMap.Isometry.snd_comp_inl {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₂ : QuadraticMap R M₂ P) :
().comp () = 0
@[simp]
theorem QuadraticMap.Isometry.fst_comp_inr {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) :
().comp () = 0
theorem QuadraticMap.Equivalent.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [] [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P} {Q₂' : QuadraticMap R N₂ P} (e₁ : Q₁.Equivalent Q₁') (e₂ : Q₂.Equivalent Q₂') :
(Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂')
@[simp]
theorem QuadraticMap.IsometryEquiv.prodComm_toFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
∀ (a : M₁ × M₂), a = a.swap
@[simp]
theorem QuadraticMap.IsometryEquiv.prodComm_invFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
∀ (a : M₂ × M₁), .invFun a = a.swap
def QuadraticMap.IsometryEquiv.prodComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
(Q₁.prod Q₂).IsometryEquiv (Q₂.prod Q₁)

LinearEquiv.prodComm is isometric.

Equations
Instances For
@[simp]
theorem QuadraticMap.IsometryEquiv.prodProdProdComm_invFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [] [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P) (Q₄ : QuadraticMap R N₂ P) (mmnn : (M₁ × N₁) × M₂ × N₂) :
().invFun mmnn = ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2)
@[simp]
theorem QuadraticMap.IsometryEquiv.prodProdProdComm_toFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [] [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P) (Q₄ : QuadraticMap R N₂ P) (mnmn : (M₁ × M₂) × N₁ × N₂) :
() mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
def QuadraticMap.IsometryEquiv.prodProdProdComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [] [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P) (Q₄ : QuadraticMap R N₂ P) :
((Q₁.prod Q₂).prod (Q₃.prod Q₄)).IsometryEquiv ((Q₁.prod Q₃).prod (Q₂.prod Q₄))

LinearEquiv.prodProdProdComm is isometric.

Equations
Instances For
theorem QuadraticMap.anisotropic_of_prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (h : (Q₁.prod Q₂).Anisotropic) :
Q₁.Anisotropic Q₂.Anisotropic

If a product is anisotropic then its components must be. The converse is not true.

theorem QuadraticMap.nonneg_prod_iff {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] [] [CovariantClass P P (fun (x x_1 : P) => x + x_1) fun (x x_1 : P) => x x_1] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} :
(∀ (x : M₁ × M₂), 0 (Q₁.prod Q₂) x) (∀ (x : M₁), 0 Q₁ x) ∀ (x : M₂), 0 Q₂ x
theorem QuadraticMap.posDef_prod_iff {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] [] [CovariantClass P P (fun (x x_1 : P) => x + x_1) fun (x x_1 : P) => x x_1] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} :
(Q₁.prod Q₂).PosDef Q₁.PosDef Q₂.PosDef
theorem QuadraticMap.PosDef.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] [] [CovariantClass P P (fun (x x_1 : P) => x + x_1) fun (x x_1 : P) => x x_1] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (h₁ : Q₁.PosDef) (h₂ : Q₂.PosDef) :
(Q₁.prod Q₂).PosDef
theorem QuadraticMap.IsOrtho.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {v : M₁ × M₂} {w : M₁ × M₂} (h₁ : Q₁.IsOrtho v.1 w.1) (h₂ : Q₂.IsOrtho v.2 w.2) :
(Q₁.prod Q₂).IsOrtho v w
@[simp]
theorem QuadraticMap.IsOrtho.inl_inr {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₁ : M₁) (m₂ : M₂) :
(Q₁.prod Q₂).IsOrtho (m₁, 0) (0, m₂)
@[simp]
theorem QuadraticMap.IsOrtho.inr_inl {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₁ : M₁) (m₂ : M₂) :
(Q₁.prod Q₂).IsOrtho (0, m₂) (m₁, 0)
@[simp]
theorem QuadraticMap.isOrtho_inl_inl_iff {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₁ : M₁) (m₁' : M₁) :
(Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) Q₁.IsOrtho m₁ m₁'
@[simp]
theorem QuadraticMap.isOrtho_inr_inr_iff {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₂ : M₂) (m₂' : M₂) :
(Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') Q₂.IsOrtho m₂ m₂'
@[simp]
theorem QuadraticMap.polar_prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (x : M₁ × M₂) (y : M₁ × M₂) :
@[simp]
theorem QuadraticMap.polarBilin_prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
(Q₁.prod Q₂).polarBilin = LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
@[simp]
theorem QuadraticMap.associated_prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R P] [] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
QuadraticMap.associated (Q₁.prod Q₂) = LinearMap.compl₁₂ (QuadraticMap.associated Q₁) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + LinearMap.compl₁₂ (QuadraticMap.associated Q₂) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
def QuadraticMap.pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) :
QuadraticMap R ((i : ι) → Mᵢ i) P

Construct a quadratic form on a family of modules from the quadratic form on each module.

Equations
• = i : ι, (Q i).comp ()
Instances For
@[simp]
theorem QuadraticMap.pi_apply {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (x : (i : ι) → Mᵢ i) :
() x = i : ι, (Q i) (x i)
theorem QuadraticMap.pi_apply_single {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] [] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (i : ι) (m : Mᵢ i) :
() () = (Q i) m
@[simp]
theorem QuadraticMap.IsometryEquiv.pi_toLinearEquiv {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} {Nᵢ : ιType u_9} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Module R P] [] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P} (e : (i : ι) → (Q i).IsometryEquiv (Q' i)) :
.toLinearEquiv = LinearEquiv.piCongrRight fun (i : ι) => (e i).toLinearEquiv
def QuadraticMap.IsometryEquiv.pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} {Nᵢ : ιType u_9} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Module R P] [] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P} (e : (i : ι) → (Q i).IsometryEquiv (Q' i)) :
().IsometryEquiv ()

An isometry between quadratic forms generated by QuadraticMap.pi can be constructed from a pair of isometries between the left and right parts.

Equations
Instances For
@[simp]
theorem QuadraticMap.Isometry.single_apply {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] [] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (i : ι) (x : Mᵢ i) (j : ι) :
x j = Pi.single i x j
def QuadraticMap.Isometry.single {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] [] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (i : ι) :
Q i →qᵢ

LinearMap.single as an isometry.

Equations
• = { toLinearMap := , map_app' := }
Instances For
@[simp]
theorem QuadraticMap.Isometry.proj_apply {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] [] (i : ι) (Q : QuadraticMap R (Mᵢ i) P) (f : (x : ι) → Mᵢ x) :
f = f i
def QuadraticMap.Isometry.proj {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] [] (i : ι) (Q : QuadraticMap R (Mᵢ i) P) :

LinearMap.proj as an isometry, when all but one quadratic form is zero.

Equations
• = { toLinearMap := , map_app' := }
Instances For
@[simp]
theorem QuadraticMap.Isometry.proj_comp_single_of_same {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] [] (i : ι) (Q : QuadraticMap R (Mᵢ i) P) :
.comp () =

Note that QuadraticMap.Isometry.id would not be well-typed as the RHS.

@[simp]
theorem QuadraticMap.Isometry.proj_comp_single_of_ne {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] [] {i : ι} {j : ι} (h : i j) (Q : QuadraticMap R (Mᵢ i) P) :
.comp () =

Note that 0 : 0 →qᵢ Q alone would not be well-typed as the RHS.

theorem QuadraticMap.Equivalent.pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} {Nᵢ : ιType u_9} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Module R P] [] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P} (e : ∀ (i : ι), (Q i).Equivalent (Q' i)) :
().Equivalent ()
theorem QuadraticMap.anisotropic_of_pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} (h : ().Anisotropic) (i : ι) :
(Q i).Anisotropic

If a family is anisotropic then its components must be. The converse is not true.

theorem QuadraticMap.nonneg_pi_iff {ι : Type u_1} {R : Type u_2} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] {P : Type u_10} [] [Module R P] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} :
(∀ (x : (i : ι) → Mᵢ i), 0 () x) ∀ (i : ι) (x : Mᵢ i), 0 (Q i) x
theorem QuadraticMap.posDef_pi_iff {ι : Type u_1} {R : Type u_2} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] {P : Type u_10} [] [Module R P] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} :
().PosDef ∀ (i : ι), (Q i).PosDef
@[simp]
theorem QuadraticMap.Ring.polar_pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommGroup (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (x : (i : ι) → Mᵢ i) (y : (i : ι) → Mᵢ i) :
QuadraticMap.polar (()) x y = i : ι, QuadraticMap.polar ((Q i)) (x i) (y i)
@[simp]
theorem QuadraticMap.Ring.polarBilin_pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommGroup (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) :
().polarBilin = i : ι, LinearMap.compl₁₂ (Q i).polarBilin () ()
@[simp]
theorem QuadraticMap.Ring.associated_pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ιType u_8} [] [(i : ι) → AddCommGroup (Mᵢ i)] [] [(i : ι) → Module R (Mᵢ i)] [Module R P] [] [] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) :
QuadraticMap.associated () = i : ι, LinearMap.compl₁₂ (QuadraticMap.associated (Q i)) () ()