gen₂

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.AdjoinPair.gen₂

English

gen₂ is the second generator of the intermediate field K⟮x, y⟯ associated with y.

Русский

gen₂ — второй генератор промежуточного поля K⟮x, y⟯, связанный с y.

LaTeX

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

Lean4

/-- The second generator of an intermediate field of the form `K⟮x, y⟯`. -/
def gen₂ : K⟮x, y⟯ :=
  ⟨y, mem_adjoin_pair_right K x y⟩

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

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

Разделы

Аффилиация

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