tmul_tensorComm_apply — Mathlib

English

The value of f.tmul g on x equals the application of the linear map of the tensor product, i.e., f.tmul g x = TensorProduct.map f.toLinearMap g.toLinearMap x.

Русский

Значение f.tmul g на x равно приложению линейной карты тензорного произведения: f.tmul g x = TensorProduct.map f.toLinearMap g.toLinearMap x.

LaTeX

$$$f.tmul g x = TensorProduct.map f.toLinearMap g.toLinearMap x$$$

Lean4

@[simp]
theorem tmul_tensorComm_apply (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (x : M₁ ⊗[R] M₂) :
    Q₂.tmul Q₁ (TensorProduct.comm R M₁ M₂ x) = Q₁.tmul Q₂ x :=
  DFunLike.congr_fun (tmul_comp_tensorComm Q₁ Q₂) x

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