case intro
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✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsIntegral { x // x ∈ subfield 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✝ : Finite G
x : F
⊢ IsIntegral { x // x ∈ subfield G F } x
cases nonempty_fintype G
no goals
case intro
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✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsIntegral { x // x ∈ subfield G F } x
exact ⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩