English
The tmul operation on isometries applies by TensorProduct.map at the level of the underlying linear maps; i.e., f.tmul g x equals TensorProduct.map f.toLinearMap g.toLinearMap x.
Русский
Операция tmul на изометриях действует через отображение TensorProduct.map на линейные карты: f.tmul g x = TensorProduct.map f.toLinearMap g.toLinearMap x.
LaTeX
$$$f : Q_1 \\to q\\!\\!\\!i Q_2$, $g : Q_3 \\to q\\!\\!\\!i Q_4$, $x$, \\\\; $f.tmul g x = TensorProduct.map f.toLinearMap g.toLinearMap x$$$
Lean4
@[simp]
theorem _root_.QuadraticMap.Isometry.tmul_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₃) :
f.tmul g x = TensorProduct.map f.toLinearMap g.toLinearMap x :=
rfl