inf_eq_bot

Mathlib.RingTheory.LinearDisjoint

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

English

If A is linearly disjoint from itself and every pair of elements in A commutes, then A is the bottom subalgebra.

Русский

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

LaTeX

$$A = ⊥$$

Lean4

theorem inf_eq_bot (H : A.LinearDisjoint B) : A ⊓ B = ⊥ :=
  H.inf_eq_bot_of_commute fun _ _ ↦ mul_comm _ _

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

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

Разделы

Аффилиация

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