[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsDomain R
inst✝¹¹ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Field L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ minpoly K (↑(algebraMap S L) s) = map (algebraMap R K) (minpoly R s)
[PROOFSTEP]
refine' (eq_of_irreducible_of_monic _ _ _).symm
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsDomain R
inst✝¹¹ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Field L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ Irreducible (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
exact (Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map (monic hs)).1 (irreducible hs)
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsDomain R
inst✝¹¹ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Field L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ ↑(Polynomial.aeval (↑(algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0
[PROOFSTEP]
rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsDomain R
inst✝¹¹ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Field L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
exact (monic hs).map _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : IsDomain R
inst✝¹³ : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
inst✝¹⁰ : IsFractionRing R K
inst✝⁹ : Field L
inst✝⁸ : Algebra R L
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : IsScalarTower R K L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)
[PROOFSTEP]
let L := FractionRing S
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : IsDomain R
inst✝¹³ : Algebra R S
K : Type u_3
L✝ : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
inst✝¹⁰ : IsFractionRing R K
inst✝⁹ : Field L✝
inst✝⁸ : Algebra R L✝
inst✝⁷ : Algebra S L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : IsScalarTower R K L✝
inst✝⁴ : IsScalarTower R S L✝
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)
[PROOFSTEP]
rw [← isIntegrallyClosed_eq_field_fractions K L hs]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : IsDomain R
inst✝¹³ : Algebra R S
K : Type u_3
L✝ : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
inst✝¹⁰ : IsFractionRing R K
inst✝⁹ : Field L✝
inst✝⁸ : Algebra R L✝
inst✝⁷ : Algebra S L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : IsScalarTower R K L✝
inst✝⁴ : IsScalarTower R S L✝
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
⊢ minpoly K s = minpoly K (↑(algebraMap S L) s)
[PROOFSTEP]
refine' minpoly.eq_of_algebraMap_eq (IsFractionRing.injective S L) (isIntegral_of_isScalarTower hs) rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
⊢ minpoly R s ∣ p
[PROOFSTEP]
let K := FractionRing R
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
⊢ minpoly R s ∣ p
[PROOFSTEP]
let L := FractionRing S
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly R s ∣ p
[PROOFSTEP]
have : minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (p %ₘ minpoly R s) :=
  by
  rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
  refine' dvd_sub (minpoly.dvd K (algebraMap S L s) _) _
  rw [← map_aeval_eq_aeval_map, hp, map_zero]
  rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
  apply dvd_mul_of_dvd_left
  rw [isIntegrallyClosed_eq_field_fractions K L hs]
  exact Monic.map _ (minpoly.monic hs)
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
[PROOFSTEP]
rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣
    map (algebraMap R K) p -
      map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
refine' dvd_sub (minpoly.dvd K (algebraMap S L s) _) _
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ ↑(Polynomial.aeval (↑(algebraMap S L) s)) (map (algebraMap R K) p) = 0
case refine'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣
    map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
rw [← map_aeval_eq_aeval_map, hp, map_zero]
[GOAL]
case refine'_1.h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ RingHom.comp (algebraMap K ((fun x => L) s)) (algebraMap R K) = RingHom.comp (algebraMap S L) (algebraMap R S)
case refine'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣
    map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣
    map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
apply dvd_mul_of_dvd_left
[GOAL]
case refine'_2.h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
rw [isIntegrallyClosed_eq_field_fractions K L hs]
[GOAL]
case _hq
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ Monic (map (algebraMap R K) (minpoly R s))
[PROOFSTEP]
exact Monic.map _ (minpoly.monic hs)
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
⊢ minpoly R s ∣ p
[PROOFSTEP]
rw [isIntegrallyClosed_eq_field_fractions _ _ hs,
  map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)] at this 
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this✝ : minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
this : minpoly R s ∣ p %ₘ minpoly R s
⊢ minpoly R s ∣ p
[PROOFSTEP]
rw [← dvd_iff_modByMonic_eq_zero (minpoly.monic hs)]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : ↑(Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this✝ : minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
this : minpoly R s ∣ p %ₘ minpoly R s
⊢ p %ₘ minpoly R s = 0
[PROOFSTEP]
refine' Polynomial.eq_zero_of_dvd_of_degree_lt this (degree_modByMonic_lt p <| minpoly.monic hs)
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsIntegrallyClosed R
inst✝ : Nontrivial R
s : S
hs : IsIntegral R s
p : R[X]
hp : minpoly R s ∣ p
⊢ ↑(Polynomial.aeval s) p = 0
[PROOFSTEP]
simpa only [RingHom.mem_ker, RingHom.coe_comp, coe_evalRingHom, coe_mapRingHom, Function.comp_apply, eval_map, ←
  aeval_def] using aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
⊢ RingHom.ker ↑(Polynomial.aeval s) = Ideal.span {minpoly R s}
[PROOFSTEP]
ext p
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
⊢ p ∈ RingHom.ker ↑(Polynomial.aeval s) ↔ p ∈ Ideal.span {minpoly R s}
[PROOFSTEP]
simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, isIntegrallyClosed_dvd_iff hs, ←
  Ideal.mem_span_singleton]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : ↑(Polynomial.aeval s) p = 0
⊢ degree (minpoly R s) ≤ degree p
[PROOFSTEP]
rw [degree_eq_natDegree (minpoly.ne_zero hs), degree_eq_natDegree hp0]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : ↑(Polynomial.aeval s) p = 0
⊢ ↑(natDegree (minpoly R s)) ≤ ↑(natDegree p)
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : ↑(Polynomial.aeval s) p = 0
⊢ natDegree (minpoly R s) ≤ natDegree p
[PROOFSTEP]
exact natDegree_le_of_dvd ((isIntegrallyClosed_dvd_iff hs _).mp hp) hp0
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
⊢ P = minpoly R s
[PROOFSTEP]
have hs : IsIntegral R s := ⟨P, hmo, hP⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
⊢ P = minpoly R s
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
⊢ minpoly R s = P
[PROOFSTEP]
apply eq_of_sub_eq_zero
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
⊢ minpoly R s - P = 0
[PROOFSTEP]
by_contra hnz
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ False
[PROOFSTEP]
have := IsIntegrallyClosed.degree_le_of_ne_zero hs hnz (by simp [hP])
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ ↑(Polynomial.aeval s) (minpoly R s - P) = 0
[PROOFSTEP]
simp [hP]
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
this : degree (minpoly R s) ≤ degree (minpoly R s - P)
⊢ False
[PROOFSTEP]
contrapose! this
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
this : ¬False
⊢ degree (minpoly R s - P) < degree (minpoly R s)
[PROOFSTEP]
refine' degree_sub_lt _ (ne_zero hs) _
[GOAL]
case h.refine'_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
this : ¬False
⊢ degree (minpoly R s) = degree P
[PROOFSTEP]
exact le_antisymm (min R s hmo hP) (Pmin (minpoly R s) (monic hs) (aeval R s))
[GOAL]
case h.refine'_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
P : R[X]
hmo : Monic P
hP : ↑(Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Monic Q → ↑(Polynomial.aeval s) Q = 0 → degree P ≤ degree Q
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
this : ¬False
⊢ leadingCoeff (minpoly R s) = leadingCoeff P
[PROOFSTEP]
rw [(monic hs).leadingCoeff, hmo.leadingCoeff]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ Prime (minpoly R x)
[PROOFSTEP]
refine'
  ⟨(minpoly.monic hx).ne_zero,
    ⟨fun h_contra => (ne_of_lt (minpoly.degree_pos hx)) (degree_eq_zero_of_isUnit h_contra).symm, fun a b h =>
      or_iff_not_imp_left.mpr fun h' => _⟩⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : minpoly R x ∣ a * b
h' : ¬minpoly R x ∣ a
⊢ minpoly R x ∣ b
[PROOFSTEP]
rw [← minpoly.isIntegrallyClosed_dvd_iff hx] at h' h ⊢
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : ↑(Polynomial.aeval x) (a * b) = 0
h' : ¬↑(Polynomial.aeval x) a = 0
⊢ ↑(Polynomial.aeval x) b = 0
[PROOFSTEP]
rw [aeval_mul] at h 
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : ↑(Polynomial.aeval x) a * ↑(Polynomial.aeval x) b = 0
h' : ¬↑(Polynomial.aeval x) a = 0
⊢ ↑(Polynomial.aeval x) b = 0
[PROOFSTEP]
exact eq_zero_of_ne_zero_of_mul_left_eq_zero h' h
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ Injective ↑(Minpoly.toAdjoin R x)
[PROOFSTEP]
refine' (injective_iff_map_eq_zero _).2 fun P₁ hP₁ => _
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : ↑(Minpoly.toAdjoin R x) P₁ = 0
⊢ P₁ = 0
[PROOFSTEP]
obtain ⟨P, hP⟩ := mk_surjective (minpoly.monic hx) P₁
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : ↑(Minpoly.toAdjoin R x) P₁ = 0
P : R[X]
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
⊢ P₁ = 0
[PROOFSTEP]
by_cases hPzero : P = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : ↑(Minpoly.toAdjoin R x) P₁ = 0
P : R[X]
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
hPzero : P = 0
⊢ P₁ = 0
[PROOFSTEP]
simpa [hPzero] using hP.symm
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : ↑(Minpoly.toAdjoin R x) P₁ = 0
P : R[X]
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
hPzero : ¬P = 0
⊢ P₁ = 0
[PROOFSTEP]
rw [← hP, Minpoly.toAdjoin_apply', liftHom_mk, ← Subalgebra.coe_eq_zero, aeval_subalgebra_coe,
  isIntegrallyClosed_dvd_iff hx] at hP₁ 
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
P : R[X]
hP₁ : minpoly R x ∣ P
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
hPzero : ¬P = 0
⊢ P₁ = 0
[PROOFSTEP]
obtain ⟨Q, hQ⟩ := hP₁
[GOAL]
case neg.intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
P : R[X]
hP : ↑(AdjoinRoot.mk (minpoly R x)) P = P₁
hPzero : ¬P = 0
Q : R[X]
hQ : P = minpoly R x * Q
⊢ P₁ = 0
[PROOFSTEP]
rw [← hP, hQ, RingHom.map_mul, mk_self, zero_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ (adjoin.powerBasis' hx).gen = { val := x, property := (_ : x ∈ adjoin R {x}) }
[PROOFSTEP]
rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin, AlgEquiv.ofBijective_apply,
  Minpoly.toAdjoin, liftHom_root]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : B.gen ∈ adjoin R {x}
⊢ (PowerBasis.ofGenMemAdjoin' B hint hx).gen = x
[PROOFSTEP]
simp [PowerBasis.ofGenMemAdjoin']
