bot_right

Mathlib.LinearAlgebra.LinearDisjoint

URI: https://scilib.ai/kg/mathlib#Submodule.LinearDisjoint.bot_right

← MathLib Explorer

English

Any M is linearly disjoint with the bottom submodule ⊥.

Русский

Любой M линейно несовместим с нижним подмодулем ⊥.

LaTeX

$$M.LinearDisjoint (⊥ : Submodule R S)$$

Lean4

/-- The zero module is linearly disjoint with any other submodules. -/
theorem bot_right : M.LinearDisjoint (⊥ : Submodule R S) :=
  ⟨Function.injective_of_subsingleton _⟩

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

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

Разделы

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

Аффилиация

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