eq_bot_of_self

Mathlib.RingTheory.LinearDisjoint

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

English

If A is linearly disjoint from itself, then A equals the bottom subalgebra.

Русский

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

LaTeX

$$A = ⊥$$

Lean4

theorem eq_bot_of_self (H : A.LinearDisjoint A) : A = ⊥ :=
  H.eq_bot_of_commute_of_self fun _ _ ↦ mul_comm _ _

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

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

Разделы

Аффилиация

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