A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ natDegree (minpoly A x) ≠ 0
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ 0 < natDegree (minpoly A x)
rw [pos_iff_ne_zero]
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ False
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ natDegree (minpoly A x) ≠ 0
intro ndeg_eq_zero
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
eq_one : minpoly A x = 1
⊢ False
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ False
have eq_one : minpoly A x = 1 := by
  rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
  convert C_1 (R := A)
  simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff
no goals
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
eq_one : minpoly A x = 1
⊢ False
simpa only [eq_one, AlgHom.map_one, one_ne_zero] using aeval A x
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ ↑C (coeff (minpoly A x) 0) = 1
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ minpoly A x = 1
rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
case h.e'_2.h.e'_6
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ coeff (minpoly A x) 0 = 1
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ ↑C (coeff (minpoly A x) 0) = 1
convert C_1 (R := A)
no goals
case h.e'_2.h.e'_6
A : Type u_2
B : Type u_1
B' : Type ?u.58941
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ coeff (minpoly A x) 0 = 1
simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff