eq_bot_of_self

Mathlib.FieldTheory.LinearDisjoint

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

← MathLib Explorer

English

If A is linearly disjoint from itself over F, then A equals F.

Русский

Если A линейно разобщено с самим собой над F, то A = F.

LaTeX

$$$A \perp_F A \Rightarrow A = F$$$

Lean4

/-- If `A` and `A` itself are linearly disjoint over `F`, then it is equal to `F`. -/
theorem eq_bot_of_self (H : A.LinearDisjoint A) : A = ⊥ :=
  inf_idem A ▸ H.inf_eq_bot

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

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

Разделы

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

Аффилиация

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