tmul_apply — Mathlib

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

Похожие утверждения