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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ f = 1 ∨ g = 1
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
⊢ f = 1 ∨ g = 1
have hf2 : f ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_right _ _
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
⊢ f = 1 ∨ g = 1
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ f = 1 ∨ g = 1
have hg2 : g ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_left _ _
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x (minpoly G F x) = 0
⊢ f = 1 ∨ g = 1
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
⊢ f = 1 ∨ g = 1
have := eval₂ 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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this :
  Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0 ∨
    Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1 ∨ g = 1
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x (minpoly G F x) = 0
⊢ f = 1 ∨ g = 1
rw [← hfg, Polynomial.eval₂_mul, mul_eq_zero] at this
case inl
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
⊢ f = 1 ∨ g = 1

case inr
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1 ∨ g = 1
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this :
  Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0 ∨
    Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1 ∨ g = 1
cases' this with this this
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
⊢ f ∣ f * g
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
⊢ f ∣ minpoly G F x
rw [← hfg]
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
⊢ f ∣ f * g
exact dvd_mul_right _ _
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ f * g
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ minpoly G F x
rw [← hfg]
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ f * g
exact dvd_mul_left _ _
case inl.h
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
⊢ g = 1
case inl
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
⊢ f = 1 ∨ g = 1
right
case inl.h
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
hf3 : f = minpoly G F x
⊢ g = 1
case inl.h
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
⊢ g = 1
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)
no goals
case inl.h
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
hf3 : f = minpoly G F x
⊢ g = 1
rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg
case inr.h
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1
case inr
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1 ∨ g = 1
left
case inr.h
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
hg3 : g = minpoly G F x
⊢ f = 1
case inr.h
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1
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)
no goals
case inr.h
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
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
hg3 : g = minpoly G F x
⊢ f = 1
rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg