English
The tensor product of two quadratic maps distributes over tmul; the tmul-tensor distributes tmul of Q1 and Q2 equals the product of their evaluations on components.
Русский
Тензорное произведение двух квадратичных отображений распределяется по tmul; tmul-tensor распределяет значения на компонентах.
LaTeX
$$$tensorDistrib\, R\, A\, (Q_1 \otimes_\text{tmul} Q_2)\, (m_1 \otimes_\text{tmul} m_2) = Q_1(m_1) \otimes_\text{tmul} Q_2(m_2)$$$
Lean4
@[simp]
theorem tensorDistrib_tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) :
tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ :=
letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
(BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <|
congr_arg₂ _ (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)
