English
The associated map of the product equals the sum of the associated maps of each factor, projected to the corresponding component.
Русский
Ассоциированная карта произведения равна сумме ассоциированных карт каждой компоненты, приведённых к соответствующим частям.
LaTeX
$$$ \\mathrm{associated}(Q_1 \\text{ prod } Q_2) = \\mathrm{associated}(Q_1) \\circ_{12} (\\mathrm{fst},\\mathrm{fst}) + \\mathrm{associated}(Q_2) \\circ_{12} (\\mathrm{snd},\\mathrm{snd}). $$$
Lean4
@[simp]
theorem associated_prod [Invertible (2 : R)] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) :
associated (Q₁.prod Q₂) =
(associated Q₁).compl₁₂ (.fst R M₁ M₂) (.fst R M₁ M₂) + (associated Q₂).compl₁₂ (.snd R M₁ M₂) (.snd R M₁ M₂) :=
by
dsimp [associated, associatedHom]
rw [polarBilin_prod, smul_add]
rfl
