eq_bot_of_commute_of_self

Mathlib.RingTheory.LinearDisjoint

URI: https://scilib.ai/kg/mathlib#Subalgebra.LinearDisjoint.eq_bot_of_commute_of_self

← MathLib Explorer

English

If A and B are linearly disjoint, then their intersection is the bottom subalgebra.

Русский

Если A и B линейно независимы, пересечение равно нижнему подалгебре.

LaTeX

$$A \\cap B = \\bot$$

Lean4

theorem eq_bot_of_commute_of_self (H : A.LinearDisjoint A) (hc : ∀ (a b : A), Commute a.1 b.1) : A = ⊥ :=
  by
  rw [← inf_of_le_left (le_refl A)] at hc ⊢
  exact H.inf_eq_bot_of_commute hc

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

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

Разделы

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

Аффилиация

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