mem_adjoin_pair_left

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.mem_adjoin_pair_left

English

x belongs to the intermediate field generated by x and y: x ∈ K⟮x, y⟯.

Русский

x принадлежит промежуточному полю, порождаемому x и y: x ∈ K⟮x, y⟯.

LaTeX

$$x \in K⟮x,y⟯$$

Lean4

theorem mem_adjoin_pair_left : x ∈ K⟮x, y⟯ :=
  subset_adjoin K { x, y } (Set.mem_insert x { y })

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

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

Разделы

Аффилиация

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