English
The polar bilinear form of the tmul of Q1 and Q2 equals the tensor product of the polar bilinear forms, scaled by 1/2.
Русский
Полярная билинейная форма tmul образует Q1 ⊗ Q2 как произведение полярных форм, умноженное на 1/2.
LaTeX
$$$\\text{polarBilin}(Q_1 \\otimes Q_2) = \\tfrac{1}{2} \\; \\text{BilinForm.tmul}(\\text{polarBilin}(Q_1), \\text{polarBilin}(Q_2))$$$
Lean4
theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
(Q₁.tmul Q₂).associated = BilinForm.tmul Q₁.associated Q₂.associated :=
by
rw [BilinForm.tmul, BilinForm.tensorDistrib, LinearMap.comp_apply, ← BilinMap.tmul, ←
QuadraticMap.associated_tmul Q₁ Q₂]
aesop