gen₁

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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