adjoin_root_eq_top — Mathlib

English

For an irreducible polynomial p over K, the intermediate field generated by AdjoinRoot.root p is the top field.

Русский

Для ирредуцируемого многочлена p над K полное промежуточное поле, порождаемое AdjoinRoot.root p, совпадает с верхним полем.

LaTeX

$$$\text{adjoinRoot }(\text{root } p) = \top$$$

Lean4

theorem adjoin_root_eq_top (p : K[X]) [Fact (Irreducible p)] : K⟮AdjoinRoot.root p⟯ = ⊤ :=
  (eq_adjoin_of_eq_algebra_adjoin K _ ⊤ (AdjoinRoot.adjoinRoot_eq_top (f := p)).symm).symm

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