R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ minpoly K (root f) = f * ↑C (Polynomial.leadingCoeff f)⁻¹
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (root f) = f * ↑C (Polynomial.leadingCoeff f)⁻¹
have f'_monic : Monic _ := monic_mul_leadingCoeff_inv hf
case refine'_1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ ↑(aeval (root f)) (f * ↑C (Polynomial.leadingCoeff f)⁻¹) = 0

case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ ∀ (q : K[X]), Monic q → ↑(aeval (root f)) q = 0 → degree (f * ↑C (Polynomial.leadingCoeff f)⁻¹) ≤ degree q
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ minpoly K (root f) = f * ↑C (Polynomial.leadingCoeff f)⁻¹
refine' (minpoly.unique K _ f'_monic _ _).symm
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
⊢ degree (f * ↑C (Polynomial.leadingCoeff f)⁻¹) ≤ degree q
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ ∀ (q : K[X]), Monic q → ↑(aeval (root f)) q = 0 → degree (f * ↑C (Polynomial.leadingCoeff f)⁻¹) ≤ degree q
intro q q_monic q_aeval
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ natDegree f ≤ natDegree q

case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ ↑C (Polynomial.leadingCoeff f)⁻¹ ≠ 0
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ degree (f * ↑C (Polynomial.leadingCoeff f)⁻¹) ≤ degree q
rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero,
  Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_le_coe, natDegree_mul hf, natDegree_C, add_zero]
case refine'_2.h1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ f ∣ q

case refine'_2.h2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ q ≠ 0

case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ ↑C (Polynomial.leadingCoeff f)⁻¹ ≠ 0
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ natDegree f ≤ natDegree q

case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ ↑C (Polynomial.leadingCoeff f)⁻¹ ≠ 0
apply natDegree_le_of_dvd
no goals
case refine'_1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ ↑(aeval (root f)) (f * ↑C (Polynomial.leadingCoeff f)⁻¹) = 0
rw [AlgHom.map_mul, aeval_eq, mk_self, MulZeroClass.zero_mul]
case h₁.a
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
x✝ : K
⊢ ↑(RingHom.comp (RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q)) C) x✝ =
    ↑(RingHom.comp (mk f) C) x✝

case h₂
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
⊢ ↑(RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q)) X = ↑(mk f) X
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
⊢ RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
ext
case h₁.a
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
x✝ : K
⊢ ↑(algebraMap K (AdjoinRoot f)) x✝ = ↑(of f) x✝
case h₁.a
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
x✝ : K
⊢ ↑(RingHom.comp (RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q)) C) x✝ =
    ↑(RingHom.comp (mk f) C) x✝
simp only [RingHom.comp_apply, mk_C, lift_of]
no goals
case h₁.a
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
x✝ : K
⊢ ↑(algebraMap K (AdjoinRoot f)) x✝ = ↑(of f) x✝
rfl
no goals
case h₂
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
⊢ ↑(RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q)) X = ↑(mk f) X
simp only [RingHom.comp_apply, mk_X, lift_root]
case refine'_2.h1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
this : ↑(mk f) q = 0
⊢ f ∣ q
case refine'_2.h1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ f ∣ q
have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]
no goals
case refine'_2.h1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
this : ↑(mk f) q = 0
⊢ f ∣ q
exact mk_eq_zero.1 this
no goals
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ ↑(mk f) q = 0
rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]
no goals
case refine'_2.h2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ q ≠ 0
exact q_monic.ne_zero
no goals
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ ↑C (Polynomial.leadingCoeff f)⁻¹ ≠ 0
rwa [Ne.def, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]