gen — Mathlib

English

The simple field generated by α and β equals the simple field generated by α and β together: F⟮α⟯⟮β⟯.restrictScalars F = F⟮α, β⟯.

Русский

Пусть α и β: простое расширение F(α)(β) эквивалентно F(α,β) — одно и то же поле.

LaTeX

$$$\\\\operatorname{adjoin}_{F}(\\\\{\\\\alpha\\\\} ) (\\\\{\\\\beta\\\\}) .\\\\restrictScalars F = \\\\operatorname{adjoin}_F (\\\\{\\\\alpha, \\\\beta\\\\}).$$$

Lean4

/-- generator of `F⟮α⟯` -/
def gen : F⟮α⟯ :=
  ⟨α, mem_adjoin_simple_self F α⟩

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