instNumberFieldRat — Mathlib

English

For any irreducible polynomial f over ℚ, the quotient field ℚ[X]/(f) is a number field; in particular, AdjoinRoot f is a number field.

Русский

Для любого неприводимого многочлена f над ℚ, отношение ℚ[X]/(f) является числовым полем; AdjoinRoot f — число поле.

LaTeX

$$$\\text{AdjoinRoot}(f) \\text{ is a NumberField for any irreducible } f ∈ \\mathbb{Q}[X].$$$

Lean4

/-- The quotient of `ℚ[X]` by the ideal generated by an irreducible polynomial of `ℚ[X]`
is a number field. -/
instance {f : Polynomial ℚ} [hf : Fact (Irreducible f)] : NumberField (AdjoinRoot f)
    where
  to_charZero := charZero_of_injective_algebraMap (algebraMap ℚ _).injective
  to_finiteDimensional := by convert (AdjoinRoot.powerBasis hf.out.ne_zero).finite

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