self_right

Mathlib.FieldTheory.LinearDisjoint

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

English

An intermediate field A is always linearly disjoint from the base field F inside E.

Русский

Любое промежуточное поле A всегда линейно неразделимо от базового поля F внутри расширения E.

LaTeX

$$$A.LinearDisjoint F.$$$

Lean4

theorem self_right : A.LinearDisjoint F :=
  Subalgebra.LinearDisjoint.bot_right _

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

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

Разделы

Аффилиация

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