mulMap_range

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

URI: https://scilib.ai/kg/mathlib#Subalgebra.mulMap_range

English

The range of the multiplication map equals the join of the subalgebras A and B.

Русский

Образ мапы умножения равен объединению подалгебр A и B.

LaTeX

$$$\operatorname{range}(A.mulMap B) = A \sqcup B$$$

Lean4

theorem mulMap_range : (A.mulMap B).range = A ⊔ B := by
  simp_rw [mulMap, Algebra.TensorProduct.productMap_range, Subalgebra.range_val]

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

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

Разделы

Аффилиация

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