English
The associated quadratic form of a tmul is the tmul of associated forms: (Q1 ⊗ Q2).associated = Q1.associated ⊗ Q2.associated.
Русский
Связанная квадратичная форма tmul равна tmul связанных форм.
LaTeX
$$$\\text{associated}(Q_1 \\otimes Q_2) = \\text{associated}(Q_1) \\otimes \\text{associated}(Q_2)$$$
Lean4
theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) :
(Q₁.tmul Q₂).associated = Q₁.associated.tmul Q₂.associated :=
by
letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
rw [QuadraticMap.tmul, BilinMap.tmul]
have : Subsingleton (Invertible (2 : A)) := inferInstance
convert
associated_left_inverse A
(LinearMap.BilinMap.tmul_isSymm (QuadraticMap.associated_isSymm A Q₁) (QuadraticMap.associated_isSymm R Q₂))
