A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ minpoly A (↑(algebraMap A B) a) = X - ↑C a
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
⊢ minpoly A (↑(algebraMap A B) a) = X - ↑C a
nontriviality A
case refine'_1
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) (X - ↑C a) = 0

case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ∀ (q : A[X]), degree q < degree (X - ↑C a) → q = 0 ∨ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ minpoly A (↑(algebraMap A B) a) = X - ↑C a
refine' (unique' A _ (monic_X_sub_C a) _ _).symm
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ∀ (q : A[X]), degree q < degree (X - ↑C a) → ¬q = 0 → ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ∀ (q : A[X]), degree q < degree (X - ↑C a) → q = 0 ∨ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
simp_rw [or_iff_not_imp_left]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : degree q < degree (X - ↑C a)
h0 : ¬q = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ∀ (q : A[X]), degree q < degree (X - ↑C a) → ¬q = 0 → ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
intro q hl h0
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : natDegree q = 0
h0 : ¬q = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : degree q < degree (X - ↑C a)
h0 : ¬q = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : natDegree q = 0
h0 : ¬↑C (coeff q 0) = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) (↑C (coeff q 0)) ≠ 0
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : natDegree q = 0
h0 : ¬q = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
rw [eq_C_of_natDegree_eq_zero hl] at h0⊢
no goals
case refine'_2
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : natDegree q = 0
h0 : ¬↑C (coeff q 0) = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) (↑C (coeff q 0)) ≠ 0
rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]
no goals
case refine'_1
A : Type u_1
B : Type u_2
B' : Type ?u.66784
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) (X - ↑C a) = 0
rw [map_sub, aeval_C, aeval_X, sub_self]