A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
hdvd : DvdNotUnit a (minpoly A x)
ha : ↑(Polynomial.aeval x) a = 0
⊢ natDegree a < natDegree (minpoly A x)
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
hdvd : DvdNotUnit a (minpoly A x)
⊢ ↑(Polynomial.aeval x) a ≠ 0
refine' fun ha => (min A x hamonic ha).not_lt (degree_lt_degree _)
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ natDegree a < natDegree (minpoly A x)
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
hdvd : DvdNotUnit a (minpoly A x)
ha : ↑(Polynomial.aeval x) a = 0
⊢ natDegree a < natDegree (minpoly A x)
obtain ⟨_, c, hu, he⟩ := hdvd
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ natDegree a < natDegree (minpoly A x)
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ natDegree a < natDegree (minpoly A x)
have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ natDegree a < natDegree a + natDegree c
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ natDegree a < natDegree (minpoly A x)
rw [he, hamonic.natDegree_mul hcm]
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ 0 < natDegree c
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ natDegree a < natDegree a + natDegree c
apply lt_add_of_pos_right
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
h : natDegree c ≤ 0
⊢ IsUnit c
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ 0 < natDegree c
refine (lt_of_not_le fun h => hu ?_)
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
h : natDegree c ≤ 0
⊢ IsUnit 1
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
h : natDegree c ≤ 0
⊢ IsUnit c
rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff,
  C_1]
no goals
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type ?u.144402
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
h : natDegree c ≤ 0
⊢ IsUnit 1
exact isUnit_one