mulMap_bot_right_eq — Mathlib

English

The product map with the bottom subalgebra on the right is the right inclusion composed with the right tensor map.

Русский

Произведение с нижним правым является композицией правой инклюзии и правого тензорного отображения.

LaTeX

$$$\text{mulMap } A \; \bot = A.{val} \circ A.rTensorBot.toAlgHom$$$

Lean4

theorem mulMap_bot_right_eq : mulMap A ⊥ = A.val.comp A.rTensorBot.toAlgHom :=
  AlgHom.toLinearMap_injective (toSubmodule A).mulMap_one_right_eq

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