case pos
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : p = 0
⊢ minpoly A x ∣ p

case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ minpoly A x ∣ p
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
⊢ minpoly A x ∣ p
by_cases hp0 : p = 0
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ minpoly A x ∣ p
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ minpoly A x ∣ p
have hx : IsIntegral A x := by
  rw [← isAlgebraic_iff_isIntegral]
  exact ⟨p, hp0, hp⟩
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ p %ₘ minpoly A x = 0
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ minpoly A x ∣ p
rw [← dvd_iff_modByMonic_eq_zero (monic hx)]
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ False
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ p %ₘ minpoly A x = 0
by_contra hnz
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
hd : degree (minpoly A x) ≤ degree (p %ₘ minpoly A x)
⊢ False
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ False
have hd := degree_le_of_ne_zero A x hnz
  ((aeval_modByMonic_eq_self_of_root (monic hx) (aeval _ _)).trans hp)
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
hd : ¬False
⊢ degree (p %ₘ minpoly A x) < degree (minpoly A x)
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
hd : degree (minpoly A x) ≤ degree (p %ₘ minpoly A x)
⊢ False
contrapose! hd
no goals
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
hd : ¬False
⊢ degree (p %ₘ minpoly A x) < degree (minpoly A x)
exact degree_modByMonic_lt _ (monic hx)
no goals
case pos
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : p = 0
⊢ minpoly A x ∣ p
simp only [hp0, dvd_zero]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ IsAlgebraic A x
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ IsIntegral A x
rw [← isAlgebraic_iff_isIntegral]
no goals
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ IsAlgebraic A x
exact ⟨p, hp0, hp⟩