M : Type u
inst✝⁵ : Monoid M
G : Type u
inst✝⁴ : Group G
F : Type v
inst✝³ : Field F
inst✝² : MulSemiringAction M F
inst✝¹ : MulSemiringAction G F
m : M
inst✝ : Fintype G
x : F
⊢ Polynomial.eval x (Polynomial.map (Subring.subtype (subfield G F).toSubring) (minpoly G F x)) =
    Polynomial.eval x (prodXSubSmul G F x)
M : Type u
inst✝⁵ : Monoid M
G : Type u
inst✝⁴ : Group G
F : Type v
inst✝³ : Field F
inst✝² : MulSemiringAction M F
inst✝¹ : MulSemiringAction G F
m : M
inst✝ : Fintype G
x : F
⊢ Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x (minpoly G F x) = 0
rw [← prodXSubSmul.eval G F x, Polynomial.eval₂_eq_eval_map]
no goals
M : Type u
inst✝⁵ : Monoid M
G : Type u
inst✝⁴ : Group G
F : Type v
inst✝³ : Field F
inst✝² : MulSemiringAction M F
inst✝¹ : MulSemiringAction G F
m : M
inst✝ : Fintype G
x : F
⊢ Polynomial.eval x (Polynomial.map (Subring.subtype (subfield G F).toSubring) (minpoly G F x)) =
    Polynomial.eval x (prodXSubSmul G F x)
simp only [minpoly, Polynomial.map_toSubring]