minpoly_eq_minpoly — Mathlib

English

The minimal polynomial of x over G F and over the fixed-point subfield are the same: minpoly G F x = minpoly (FixedPoints.subfield G F) x.

Русский

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

LaTeX

$$$\\minpoly G F x = \\minpoly( FixedPoints.subfield G F ) x$$$

Lean4

theorem minpoly_eq_minpoly : minpoly G F x = _root_.minpoly (FixedPoints.subfield G F) x :=
  minpoly.eq_of_irreducible_of_monic (minpoly.irreducible G F x) (minpoly.eval₂ G F x) (minpoly.monic G F x)

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