mulMap_eq_mul'_comp_mapIncl

Mathlib.LinearAlgebra.TensorProduct.Submodule

URI: https://scilib.ai/kg/mathlib#Submodule.mulMap_eq_mul'_comp_mapIncl

English

The forward mulMap equals the mul' map composed with mapIncl; i.e., the two constructions agree.

Русский

Прямая mulMap равна mul' ∘ mapIncl; т.е. две конструкции совпадают.

LaTeX

$$$mulMap M N = .mul' R S \circ_\ell TensorProduct.mapIncl M N$$$

Lean4

theorem mulMap_eq_mul'_comp_mapIncl : mulMap M N = .mul' R S ∘ₗ TensorProduct.mapIncl M N :=
  TensorProduct.ext' fun _ _ ↦ rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru