[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pnz : p ≠ 0
hp : ↑(Polynomial.aeval x) p = 0
⊢ ↑(Polynomial.aeval x) (p * ↑C (leadingCoeff p)⁻¹) = 0
[PROOFSTEP]
simp [hp]
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
⊢ p = minpoly A x
[PROOFSTEP]
have hx : IsIntegral A x := ⟨p, pmonic, hp⟩
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ p = minpoly A x
[PROOFSTEP]
symm
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ minpoly A x = p
[PROOFSTEP]
apply eq_of_sub_eq_zero
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ minpoly A x - p = 0
[PROOFSTEP]
by_contra hnz
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ False
[PROOFSTEP]
have hd := degree_le_of_ne_zero A x hnz (by simp [hp])
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ ↑(Polynomial.aeval x) (minpoly A x - p) = 0
[PROOFSTEP]
simp [hp]
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : degree (minpoly A x) ≤ degree (minpoly A x - p)
⊢ False
[PROOFSTEP]
contrapose! hd
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ degree (minpoly A x - p) < degree (minpoly A x)
[PROOFSTEP]
apply degree_sub_lt _ (minpoly.ne_zero hx)
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ leadingCoeff (minpoly A x) = leadingCoeff p
[PROOFSTEP]
rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ degree (minpoly A x) = degree p
[PROOFSTEP]
exact le_antisymm (min A x pmonic hp) (pmin (minpoly A x) (monic hx) (aeval A x))
[GOAL]
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
[PROOFSTEP]
by_cases hp0 : p = 0
[GOAL]
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
[PROOFSTEP]
simp only [hp0, dvd_zero]
[GOAL]
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
[PROOFSTEP]
have hx : IsIntegral A x := by
  rw [← isAlgebraic_iff_isIntegral]
  exact ⟨p, hp0, hp⟩
[GOAL]
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
[PROOFSTEP]
rw [← isAlgebraic_iff_isIntegral]
[GOAL]
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
[PROOFSTEP]
exact ⟨p, hp0, hp⟩
[GOAL]
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
[PROOFSTEP]
rw [← dvd_iff_modByMonic_eq_zero (monic hx)]
[GOAL]
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
[PROOFSTEP]
by_contra hnz
[GOAL]
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
[PROOFSTEP]
have hd := degree_le_of_ne_zero A x hnz ((aeval_modByMonic_eq_self_of_root (monic hx) (aeval _ _)).trans hp)
[GOAL]
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
[PROOFSTEP]
contrapose! hd
[GOAL]
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)
[PROOFSTEP]
exact degree_modByMonic_lt _ (monic hx)
[GOAL]
A✝ : Type u_1
B : Type u_2
inst✝⁹ : Field A✝
inst✝⁸ : Ring B
inst✝⁷ : Algebra A✝ B
x✝ : B
A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : CommRing R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ minpoly K x ∣ map (algebraMap A K) (minpoly A x)
[PROOFSTEP]
refine' minpoly.dvd K x _
[GOAL]
A✝ : Type u_1
B : Type u_2
inst✝⁹ : Field A✝
inst✝⁸ : Ring B
inst✝⁷ : Algebra A✝ B
x✝ : B
A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : CommRing R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ ↑(Polynomial.aeval x) (map (algebraMap A K) (minpoly A x)) = 0
[PROOFSTEP]
rw [aeval_map_algebraMap, minpoly.aeval]
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)
[PROOFSTEP]
apply minpoly.dvd K (algebraMap S L s)
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ ↑(Polynomial.aeval (↑(algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0
[PROOFSTEP]
rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ RingHom.comp (algebraMap K ((fun x => L) s)) (algebraMap R K) = RingHom.comp (algebraMap S L) (algebraMap R S)
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
⊢ p * ↑C (leadingCoeff p)⁻¹ = minpoly A x
[PROOFSTEP]
have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ p * ↑C (leadingCoeff p)⁻¹ = minpoly A x
[PROOFSTEP]
apply eq_of_irreducible_of_monic
[GOAL]
case hp1
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ Irreducible (p * ↑C (leadingCoeff p)⁻¹)
[PROOFSTEP]
exact
  Associated.irreducible
    ⟨⟨C p.leadingCoeff⁻¹, C p.leadingCoeff, by rwa [← C_mul, inv_mul_cancel, C_1], by
        rwa [← C_mul, mul_inv_cancel, C_1]⟩,
      rfl⟩
    hp1
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑C (leadingCoeff p)⁻¹ * ↑C (leadingCoeff p) = 1
[PROOFSTEP]
rwa [← C_mul, inv_mul_cancel, C_1]
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑C (leadingCoeff p) * ↑C (leadingCoeff p)⁻¹ = 1
[PROOFSTEP]
rwa [← C_mul, mul_inv_cancel, C_1]
[GOAL]
case hp2
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑(Polynomial.aeval x) (p * ↑C (leadingCoeff p)⁻¹) = 0
[PROOFSTEP]
rw [aeval_mul, hp2, zero_mul]
[GOAL]
case hp3
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ Monic (p * ↑C (leadingCoeff p)⁻¹)
[PROOFSTEP]
rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel]
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x✝ : B
K : Type u_3
S : Type u_4
T : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra K S
inst✝² : Algebra K T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower K S T
hST : Injective ↑(algebraMap S T)
x : S
y : T
hx : IsIntegral K x
h : y = ↑(algebraMap S T) x
⊢ ↑(Polynomial.aeval y) (minpoly K x) = 0
[PROOFSTEP]
rw [h, aeval_algebraMap_apply, minpoly.aeval, RingHom.map_zero]
[GOAL]
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ minpoly A (x + ↑(algebraMap A B) a) = Polynomial.comp (minpoly A x) (X - ↑C a)
[PROOFSTEP]
refine' (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) _ fun q qmo hq => _).symm
[GOAL]
case refine'_1
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) (Polynomial.comp (minpoly A x) (X - ↑C a)) = 0
[PROOFSTEP]
simp [aeval_comp]
[GOAL]
case refine'_2
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
[PROOFSTEP]
have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
[GOAL]
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
⊢ ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
[PROOFSTEP]
simpa [aeval_comp] using hq
[GOAL]
case refine'_2
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
[PROOFSTEP]
have H := minpoly.min A x (qmo.comp_X_add_C _) this
[GOAL]
case refine'_2
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
H : degree (minpoly A x) ≤ degree (Polynomial.comp q (X + ↑C a))
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
[PROOFSTEP]
rw [degree_eq_natDegree qmo.ne_zero, degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
  natDegree_X_sub_C, mul_one]
[GOAL]
case refine'_2
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
H : degree (minpoly A x) ≤ degree (Polynomial.comp q (X + ↑C a))
⊢ ↑(natDegree (minpoly A x)) ≤ ↑(natDegree q)
[PROOFSTEP]
rwa [degree_eq_natDegree (minpoly.ne_zero hx), degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
  natDegree_X_add_C, mul_one] at H 
[GOAL]
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ minpoly A (x - ↑(algebraMap A B) a) = Polynomial.comp (minpoly A x) (X + ↑C a)
[PROOFSTEP]
simpa [sub_eq_add_neg] using add_algebraMap hx (-a)
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x✝ : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
φ : E →ₐ[F] K
x : ↑(range ↑(FiniteDimensional.finBasis F E))
⊢ ↑φ ↑x ∈ roots (map (algebraMap F K) (minpoly F ↑x))
[PROOFSTEP]
rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val), ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
⊢ Injective (rootsOfMinPolyPiType F E K)
[PROOFSTEP]
intro f g h
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ f = g
[PROOFSTEP]
suffices (f : E →ₗ[F] K) = g by rwa [FunLike.ext'_iff] at this ⊢
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
this : ↑↑f = ↑↑g
⊢ f = g
[PROOFSTEP]
rwa [FunLike.ext'_iff] at this ⊢
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ ↑↑f = ↑↑g
[PROOFSTEP]
rw [funext_iff] at h 
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : ∀ (a : ↑(range ↑(FiniteDimensional.finBasis F E))), rootsOfMinPolyPiType F E K f a = rootsOfMinPolyPiType F E K g a
⊢ ↑↑f = ↑↑g
[PROOFSTEP]
exact LinearMap.ext_on (FiniteDimensional.finBasis F E).span_eq fun e he => Subtype.ext_iff.mp (h ⟨e, he⟩)
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ minpoly A 0 = X
[PROOFSTEP]
simpa only [add_zero, C_0, sub_eq_add_neg, neg_zero, RingHom.map_zero] using eq_X_sub_C B (0 : A)
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ minpoly A 1 = X - 1
[PROOFSTEP]
simpa only [RingHom.map_one, C_1, sub_eq_add_neg] using eq_X_sub_C B (1 : A)
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ Prime (minpoly A x)
[PROOFSTEP]
refine' ⟨minpoly.ne_zero hx, not_isUnit A x, _⟩
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ ∀ (a b : A[X]), minpoly A x ∣ a * b → minpoly A x ∣ a ∨ minpoly A x ∣ b
[PROOFSTEP]
rintro p q ⟨d, h⟩
[GOAL]
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
[PROOFSTEP]
have : Polynomial.aeval x (p * q) = 0 := by simp [h, aeval A x]
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
⊢ ↑(Polynomial.aeval x) (p * q) = 0
[PROOFSTEP]
simp [h, aeval A x]
[GOAL]
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : ↑(Polynomial.aeval x) (p * q) = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
[PROOFSTEP]
replace : Polynomial.aeval x p = 0 ∨ Polynomial.aeval x q = 0 := by simpa
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : ↑(Polynomial.aeval x) (p * q) = 0
⊢ ↑(Polynomial.aeval x) p = 0 ∨ ↑(Polynomial.aeval x) q = 0
[PROOFSTEP]
simpa
[GOAL]
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : ↑(Polynomial.aeval x) p = 0 ∨ ↑(Polynomial.aeval x) q = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
[PROOFSTEP]
exact Or.imp (dvd A x) (dvd A x) this
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
⊢ ↑(algebraMap A B) y = x
[PROOFSTEP]
have key : minpoly A x = X - C y :=
  eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
    (associated_of_dvd_dvd ((irreducible_X_sub_C y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
      (dvd_iff_isRoot.2 h))
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = X - ↑C y
⊢ ↑(algebraMap A B) y = x
[PROOFSTEP]
have := aeval A x
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = X - ↑C y
this : ↑(Polynomial.aeval x) (minpoly A x) = 0
⊢ ↑(algebraMap A B) y = x
[PROOFSTEP]
rwa [key, AlgHom.map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this 
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ coeff (minpoly A x) 0 = 0 ↔ x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ coeff (minpoly A x) 0 = 0 → x = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
⊢ x = 0
[PROOFSTEP]
have zero_root := zero_isRoot_of_coeff_zero_eq_zero h
[GOAL]
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
zero_root : IsRoot (minpoly A x) 0
⊢ x = 0
[PROOFSTEP]
rw [← root hx zero_root]
[GOAL]
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
zero_root : IsRoot (minpoly A x) 0
⊢ ↑(algebraMap A B) 0 = 0
[PROOFSTEP]
exact RingHom.map_zero _
[GOAL]
case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ x = 0 → coeff (minpoly A x) 0 = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
hx : IsIntegral A 0
⊢ coeff (minpoly A 0) 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : x ≠ 0
⊢ coeff (minpoly A x) 0 ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
⊢ x = 0
[PROOFSTEP]
simpa only [hx, coeff_zero_eq_zero] using h
