English
If a polynomial f evaluates to zero at x with eval₂, then minpoly divides f.
Русский
Если f(x)=0 через eval₂, то minpoly делит f.
LaTeX
$$$ \\forall f, \\big( \\mathrm{Polynomial.eval₂}(\\mathrm{FixedPoints.subfield G F}.subtype, x, f) = 0 \\big) \\Rightarrow \\mathrm{minpoly}(G,F,x) \\mid f $$$
Lean4
theorem of_eval₂ (f : Polynomial (FixedPoints.subfield G F))
(hf : Polynomial.eval₂ (Subfield.subtype <| FixedPoints.subfield G F) x f = 0) : minpoly G F x ∣ f := by
classical
rw [← Polynomial.map_dvd_map' (Subfield.subtype <| FixedPoints.subfield G F), minpoly, ←
Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ _, prodXSubSMul]
refine
Fintype.prod_dvd_of_coprime (Polynomial.pairwise_coprime_X_sub_C <| MulAction.injective_ofQuotientStabilizer G x)
fun y => QuotientGroup.induction_on y fun g => ?_
rw [Polynomial.dvd_iff_isRoot, Polynomial.IsRoot.def, MulAction.ofQuotientStabilizer_mk, Polynomial.eval_smul', ←
IsInvariantSubring.coe_subtypeHom' G (FixedPoints.subfield G F).toSubring, ← MulSemiringActionHom.coe_polynomial, ←
MulSemiringActionHom.map_smul, smul_polynomial, MulSemiringActionHom.coe_polynomial,
IsInvariantSubring.coe_subtypeHom', Polynomial.eval_map, Subfield.toSubring_subtype_eq_subtype, hf, smul_zero]
-- Why is this so slow?
