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
H : minpoly G F x = 1
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x (minpoly G F x) = 0
⊢ 1 = 0
rwa [H, Polynomial.eval₂_one] at this