mulMap_one_left_eq — Mathlib

English

The map mulMap with the bottom subalgebra on the left equals the composition of N.subtype with N.lTensorOne; i.e., left multiplication by the bottom subalgebra factors through the left tensor unit.

Русский

Отображение mulMap слева от низа подалгебры равно композиции N.subtype с N.lTensorOne: разложение через левую тензорную единицу.

LaTeX

$$$mulMap (Subalgebra.toSubmodule \\top) N = N.subtype \\circ N.lTensorOne$$$

Lean4

theorem mulMap_one_left_eq : mulMap (Subalgebra.toSubmodule ⊥) N = N.subtype ∘ₗ N.lTensorOne.toLinearMap :=
  TensorProduct.ext' fun _ _ ↦ rfl

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