comm_comp_rTensor_comp_comm_eq — Mathlib

English

Compatibility of scalar action with lTensor: s • (f.lTensor M) = (f.lTensor M) (s • ·).

Русский

Совместимость скалярного действия с lTensor: s • (f.lTensor M) = (f.lTensor M) (s • ·).

LaTeX

$$$ s \\cdot (f.lTensor M) = f.lTensor M \\circ s \\mathrm{smul} $$$

Lean4

theorem comm_comp_rTensor_comp_comm_eq (g : N →ₗ[R] P) :
    TensorProduct.comm R P Q ∘ₗ rTensor Q g ∘ₗ TensorProduct.comm R Q N = lTensor Q g :=
  TensorProduct.ext rfl

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