English
There is a canonical Isometry between Q1.tmul Q3 and Q2.tmul Q4 induced by isometries f: Q1 → Q2 and g: Q3 → Q4, i.e., tmul maps are defined via f.toLinearMap and g.toLinearMap.
Русский
Существует каноническая изометрия между Q1.tmul Q3 и Q2.tmul Q4, индуцируемая изометриями f: Q1 → Q2 и g: Q3 → Q4; отображения tmul задаются через линейные карты f.toLinearMap и g.toLinearMap.
LaTeX
$$$f : Q_1 \\to q\\!\\!\\!i Q_2$, $g : Q_3 \\to q\\!\\!\\!i Q_4$ \\\\rightarrow\\; (Q_1 \\tmul Q_3) \\to q\\!\\!\\! i (Q_2 \\tmul Q_4)$ via $TensorProduct.map f.toLinearMap g.toLinearMap$$$
Lean4
@[simp]
theorem tmul_tensorMap_apply {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
{Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) (x : M₁ ⊗[R] M₃) :
Q₂.tmul Q₄ (TensorProduct.map f.toLinearMap g.toLinearMap x) = Q₁.tmul Q₃ x :=
DFunLike.congr_fun (tmul_comp_tensorMap f g) x
