mem_adjoin_pair_right

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_adjoin_pair_right : y ∈ K⟮x, y⟯ :=
  subset_adjoin K { x, y } (Set.mem_insert_of_mem x (Set.mem_singleton y))

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

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

Разделы

Аффилиация

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