rTensor_smul_action — Mathlib

English

Another formulation of map with rTensor: map f g (f' x) = map (f ∘ f') g x for appropriate x.

Русский

Ещё одно формулирование map с rTensor: map f g (f' x) = map (f ∘ f') g x.

LaTeX

$$$\text{map } f\, g\ (f'.\mathrm{rTensor}\ _\ x) = \text{map } (f \circ f')\, g\ x$$$

Lean4

@[simp]
theorem rTensor_smul_action (r : R) :
    (DistribMulAction.toLinearMap R N r).rTensor M = DistribMulAction.toLinearMap R (N ⊗[R] M) r :=
  (rTensor_smul M r LinearMap.id).trans (congrArg _ (rTensor_id M N))

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