English
Let G be a finite group acting on a field F and denote by FixedPoints.subfield G F the fixed-point subfield. For monic polynomials f and g over FixedPoints.subfield G F, if f · g equals the minimal polynomial minpoly G F x of some x ∈ F, then one of f or g must be the constant polynomial 1. In particular, minpoly G F x is irreducible over FixedPoints.subfield G F.
Русский
Пусть G — конечная группа действует на поле F, и обозначим подполе фиксированных точек FixedPoints.subfield G F. Пусть f и g — мончные многочлены над FixedPoints.subfield G F и их произведение равняется минполиному minpoly G F x для некоторого x ∈ F. Тогда либо f, либо g равно единице. Следовательно, minpoly G F x неприводим по отношению к FixedPoints.subfield G F.
LaTeX
$$$\\forall f,g \\in \\operatorname{Polynomial}(\\operatorname{FixedPoints.subfield } G F),\\ f\\text{ Monic} \\land g\\text{ Monic} \\land f \\cdot g = \\minpoly G F x\\;\\Rightarrow\\; f = 1 \\lor g = 1$$$
Lean4
theorem irreducible_aux (f g : Polynomial (FixedPoints.subfield G F)) (hf : f.Monic) (hg : g.Monic)
(hfg : f * g = minpoly G F x) : f = 1 ∨ g = 1 :=
by
have hf2 : f ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_right _ _
have hg2 : g ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_left _ _
have := eval₂ G F x
rw [← hfg, Polynomial.eval₂_mul, mul_eq_zero] at this
rcases this with this | this
· right
have hf3 : f = minpoly G F x :=
Polynomial.eq_of_monic_of_associated hf (monic G F x)
(associated_of_dvd_dvd hf2 <| @of_eval₂ G _ F _ _ _ x f this)
rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg
· left
have hg3 : g = minpoly G F x :=
Polynomial.eq_of_monic_of_associated hg (monic G F x)
(associated_of_dvd_dvd hg2 <| @of_eval₂ G _ F _ _ _ x g this)
rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg
