mulMap'_surjective

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

URI: https://scilib.ai/kg/mathlib#Subalgebra.mulMap'_surjective

← MathLib Explorer

English

Again, mulMap' is surjective onto the join A ⊔ B.

Русский

again: mulMap' сюръективен на A ⊔ B.

LaTeX

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

Lean4

theorem mulMap'_surjective : Function.Surjective (mulMap' A B) := by
  simp_rw [mulMap', AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe, EquivLike.comp_surjective,
    AlgHom.rangeRestrict_surjective]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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