irreducible — Mathlib

English

The minimal polynomial of x over the fixed-point subfield FixedPoints.subfield G F is irreducible; i.e., minpoly G F x is an irreducible polynomial in (FixedPoints.subfield G F)[t].

Русский

Минимальный полином элемента x над подполем фиксированных точек (FixedPoints.subfield G F) является неприводимым, то есть minpoly G F x неприводим по отношению к (FixedPoints.subfield G F)[t].

LaTeX

$$$\\text{Irreducible}(\\minpoly G F x)$$$

Lean4

theorem irreducible : Irreducible (minpoly G F x) :=
  (Polynomial.irreducible_of_monic (monic G F x) (ne_one G F x)).2 (irreducible_aux G F x)

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