A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
⊢ f = 1 ∨ g = 1
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
⊢ Irreducible (minpoly A x)
refine' (irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => _
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
⊢ IsUnit f ∨ IsUnit g
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
⊢ f = 1 ∨ g = 1
rw [← hf.isUnit_iff, ← hg.isUnit_iff]
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
⊢ False
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
⊢ IsUnit f ∨ IsUnit g
by_contra' h
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) (f * g) = ↑(Polynomial.aeval x) (minpoly A x)
⊢ False
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
⊢ False
have heval := congr_arg (Polynomial.aeval x) he
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) f = 0 ∨ ↑(Polynomial.aeval x) g = 0
⊢ False
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) (f * g) = ↑(Polynomial.aeval x) (minpoly A x)
⊢ False
rw [aeval A x, aeval_mul, mul_eq_zero] at heval
case inl
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) f = 0
⊢ False

case inr
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) g = 0
⊢ False
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) f = 0 ∨ ↑(Polynomial.aeval x) g = 0
⊢ False
cases' heval with heval heval
no goals
case inl
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) f = 0
⊢ False
exact aeval_ne_zero_of_dvdNotUnit_minpoly hx hf ⟨hf.ne_zero, g, h.2, he.symm⟩ heval
case inr
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) g = 0
⊢ minpoly A x = g * f
case inr
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) g = 0
⊢ False
refine' aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, _⟩ heval
no goals
case inr
A : Type u_1
B : Type u_2
B' : Type ?u.150283
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) g = 0
⊢ minpoly A x = g * f
rw [mul_comm, he]