map_comp_lTensor — Mathlib

English

A final formulation of map with rTensor: map f g (f' . rTensor x) = map (f ∘ f') g x.

Русский

Окончательная формулировка отображения map с rTensor: map f g (f' . rTensor x) = map (f ∘ f') g x.

LaTeX

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

Lean4

@[simp]
theorem map_comp_lTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) :
    (map f g).comp (g'.lTensor _) = map f (g.comp g') := by simp only [lTensor, ← map_comp, comp_id]

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