mulMap_one_right_eq — Mathlib

English

For a submodule M, the right multiplication map by the bottom subalgebra ⊥ is equal to the composition M.subtype ∘ₗ M.rTensorOne.toLinearMap.

Русский

Для подмодуля M правое умножение на нижний подалгебра ⊥ эквивалентно композиции M.subtype с линейным отображением M.rTensorOne.

LaTeX

$$$\\mathrm{mulMap}\\ M\\ (\\mathrm{Subalgebra.toSubmodule}\\ \\perp) = M.\\mathrm{subtype} \\circ_{\\ell} M.rTensorOne.toLinearMap$$$

Lean4

theorem mulMap_one_right_eq : mulMap M (Subalgebra.toSubmodule ⊥) = M.subtype ∘ₗ M.rTensorOne.toLinearMap :=
  TensorProduct.ext' fun _ _ ↦ rfl

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