bot_left

Mathlib.LinearAlgebra.LinearDisjoint

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

← MathLib Explorer

English

The bottom submodule ⊥ is linearly disjoint from any submodule N.

Русский

Нижний подмодуль ⊥ линейно несовместен с любым подмодулем N.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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