∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (Mᵢ i)] [inst_2 : AddCommGroup P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] [inst_6 : Invertible 2] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P),
  QuadraticMap.associated (QuadraticMap.pi Q) =
    ∑ i, LinearMap.compl₁₂ (QuadraticMap.associated (Q i)) (LinearMap.proj i) (LinearMap.proj i)