mulMap'_surjective

Mathlib.LinearAlgebra.TensorProduct.Submodule

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

← MathLib Explorer

English

Again, mulMap' is surjective onto A ⊔ B.

Русский

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

LaTeX

$$$\operatorname{range}(mulMap' M N) = M \sqcup N$$$

Lean4

theorem mulMap'_surjective : Function.Surjective (mulMap' M N) := by
  simp_rw [mulMap', LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective,
    LinearMap.surjective_rangeRestrict]

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

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

Разделы

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

Аффилиация

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