[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
⊢ ↑(aeval (↑(algebraMap A S) r)) (scaleRoots p ↑s) = 0
[PROOFSTEP]
convert scaleRoots_eval₂_eq_zero (algebraMap A S) hr
[GOAL]
case h.e'_2.h.e
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
⊢ ↑(aeval (↑(algebraMap A S) r)) = eval₂ (algebraMap A S) (↑(algebraMap A S) ↑s * mk' S r s)
[PROOFSTEP]
funext
[GOAL]
case h.e'_2.h.e.h
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
x✝ : A[X]
⊢ ↑(aeval (↑(algebraMap A S) r)) x✝ = eval₂ (algebraMap A S) (↑(algebraMap A S) ↑s * mk' S r s) x✝
[PROOFSTEP]
rw [aeval_def, mk'_spec' _ r s]
[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid A
inst✝⁵ : Algebra A S
inst✝⁴ : IsLocalization M S
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ IsRoot (scaleRoots p ↑(den A x)) (num A x)
[PROOFSTEP]
apply isRoot_of_eval₂_map_eq_zero (IsFractionRing.injective A K)
[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid A
inst✝⁵ : Algebra A S
inst✝⁴ : IsLocalization M S
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ eval₂ (algebraMap A K) (↑(algebraMap A K) (num A x)) (scaleRoots p ↑(den A x)) = 0
[PROOFSTEP]
refine' scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero _
[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid A
inst✝⁵ : Algebra A S
inst✝⁴ : IsLocalization M S
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ ↑(aeval (mk' K (num A x) (den A x))) p = 0
[PROOFSTEP]
rw [mk'_num_den]
[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid A
inst✝⁵ : Algebra A S
inst✝⁴ : IsLocalization M S
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ ↑(aeval x) p = 0
[PROOFSTEP]
exact hr
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ num A r ∣ coeff p 0
[PROOFSTEP]
suffices num A r ∣ (scaleRoots p (den A r)).coeff 0
  by
  simp only [coeff_scaleRoots, tsub_zero] at this
  haveI inst := Classical.propDecidable
  by_cases hr : num A r = 0
  · obtain ⟨u, hu⟩ := (isUnit_den_of_num_eq_zero hr).pow p.natDegree
    rw [← hu] at this
    exact Units.dvd_mul_right.mp this
  · refine' dvd_of_dvd_mul_left_of_no_prime_factors hr _ this
    intro q dvd_num dvd_denom_pow hq
    apply hq.not_unit
    exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : num A r ∣ coeff (scaleRoots p ↑(den A r)) 0
⊢ num A r ∣ coeff p 0
[PROOFSTEP]
simp only [coeff_scaleRoots, tsub_zero] at this
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
[PROOFSTEP]
haveI inst := Classical.propDecidable
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
⊢ num A r ∣ coeff p 0
[PROOFSTEP]
by_cases hr : num A r = 0
[GOAL]
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : num A r = 0
⊢ num A r ∣ coeff p 0
[PROOFSTEP]
obtain ⟨u, hu⟩ := (isUnit_den_of_num_eq_zero hr).pow p.natDegree
[GOAL]
case pos.intro
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : num A r = 0
u : Aˣ
hu : ↑u = ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
[PROOFSTEP]
rw [← hu] at this
[GOAL]
case pos.intro
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
inst : (a : Prop) → Decidable a
hr : num A r = 0
u : Aˣ
this : num A r ∣ coeff p 0 * ↑u
hu : ↑u = ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
[PROOFSTEP]
exact Units.dvd_mul_right.mp this
[GOAL]
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
⊢ num A r ∣ coeff p 0
[PROOFSTEP]
refine' dvd_of_dvd_mul_left_of_no_prime_factors hr _ this
[GOAL]
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
⊢ ∀ {d : A}, d ∣ num A r → d ∣ ↑(den A r) ^ natDegree p → ¬Prime d
[PROOFSTEP]
intro q dvd_num dvd_denom_pow hq
[GOAL]
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
dvd_num : q ∣ num A r
dvd_denom_pow : q ∣ ↑(den A r) ^ natDegree p
hq : Prime q
⊢ False
[PROOFSTEP]
apply hq.not_unit
[GOAL]
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
dvd_num : q ∣ num A r
dvd_denom_pow : q ∣ ↑(den A r) ^ natDegree p
hq : Prime q
⊢ IsUnit q
[PROOFSTEP]
exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ num A r ∣ coeff (scaleRoots p ↑(den A r)) 0
[PROOFSTEP]
convert dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _
[GOAL]
case h.e'_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ coeff (scaleRoots p ↑(den A r)) 0 = coeff (scaleRoots p ↑(den A r)) 0 * num A r ^ 0
[PROOFSTEP]
rw [pow_zero, mul_one]
[GOAL]
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ 0 → num A r ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
intro j hj
[GOAL]
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
apply dvd_mul_of_dvd_right
[GOAL]
case convert_2.h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ num A r ^ j
[PROOFSTEP]
convert pow_dvd_pow (num A r) (Nat.succ_le_of_lt (bot_lt_iff_ne_bot.mpr hj))
[GOAL]
case h.e'_3
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r = num A r ^ Nat.succ ⊥
[PROOFSTEP]
exact (pow_one _).symm
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ↑(den A r) ∣ leadingCoeff p
[PROOFSTEP]
suffices (den A r : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
  by
  refine' dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) _ this
  intro q dvd_den dvd_num_pow hq
  apply hq.not_unit
  exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
⊢ ↑(den A r) ∣ leadingCoeff p
[PROOFSTEP]
refine' dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) _ this
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
⊢ ∀ {d : A}, d ∣ ↑(den A r) → d ∣ num A r ^ natDegree p → ¬Prime d
[PROOFSTEP]
intro q dvd_den dvd_num_pow hq
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ natDegree p
hq : Prime q
⊢ False
[PROOFSTEP]
apply hq.not_unit
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ natDegree p
hq : Prime q
⊢ IsUnit q
[PROOFSTEP]
exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
[PROOFSTEP]
rw [← coeff_scaleRoots_natDegree]
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ↑(den A r) ∣ coeff (scaleRoots p ?s) (natDegree p) * num A r ^ natDegree p
case s
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ A
[PROOFSTEP]
apply dvd_term_of_isRoot_of_dvd_terms _ (num_isRoot_scaleRoots_of_aeval_eq_zero hr)
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ natDegree p → ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
intro j hj
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
by_cases h : j < p.natDegree
[GOAL]
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
rw [coeff_scaleRoots]
[GOAL]
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ coeff p j * ↑(den A r) ^ (natDegree p - j) * num A r ^ j
[PROOFSTEP]
refine' (dvd_mul_of_dvd_right _ _).mul_right _
[GOAL]
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ ↑(den A r) ^ (natDegree p - j)
[PROOFSTEP]
convert pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))
[GOAL]
case h.e'_3
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) = ↑(den A r) ^ Nat.succ ?pos.convert_1✝
[PROOFSTEP]
exact (pow_one _).symm
[GOAL]
case pos.convert_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ j + 0 < natDegree p
[PROOFSTEP]
simpa using h
[GOAL]
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : ¬j < natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
rw [← natDegree_scaleRoots p (den A r)] at *
[GOAL]
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree (scaleRoots p ↑(den A r))
h : ¬j < natDegree (scaleRoots p ↑(den A r))
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne (le_of_not_gt h) hj.symm), zero_mul]
[GOAL]
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree (scaleRoots p ↑(den A r))
h : ¬j < natDegree (scaleRoots p ↑(den A r))
⊢ ↑(den A r) ∣ 0
[PROOFSTEP]
exact dvd_zero _


[GOAL]
n : ℕ
z : ℂ
⊢ ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)
[PROOFSTEP]
rintro ⟨h1, h2⟩
[GOAL]
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ False
[PROOFSTEP]
replace h3 : z ^ 3 = 1
[GOAL]
case h3
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ z ^ 3 = 1
[PROOFSTEP]
linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2
[GOAL]
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ False
[PROOFSTEP]
have key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2 :=
  by
  rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]
  have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
  interval_cases n % 3 <;> simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true_iff, true_or_iff]
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
[PROOFSTEP]
rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = z ^ 2
[PROOFSTEP]
have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : n % 3 < 3
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = z ^ 2
[PROOFSTEP]
interval_cases n % 3
[GOAL]
case «0»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 0 < 3
⊢ z ^ 0 = 1 ∨ z ^ 0 = z ∨ z ^ 0 = z ^ 2
[PROOFSTEP]
simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true_iff, true_or_iff]
[GOAL]
case «1»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 1 < 3
⊢ z ^ 1 = 1 ∨ z ^ 1 = z ∨ z ^ 1 = z ^ 2
[PROOFSTEP]
simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true_iff, true_or_iff]
[GOAL]
case «2»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 2 < 3
⊢ z ^ 2 = 1 ∨ z ^ 2 = z ∨ z ^ 2 = z ^ 2
[PROOFSTEP]
simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true_iff, true_or_iff]
[GOAL]
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
⊢ False
[PROOFSTEP]
have z_ne_zero : z ≠ 0 := fun h => zero_ne_one ((zero_pow zero_lt_three).symm.trans (show (0 : ℂ) ^ 3 = 1 from h ▸ h3))
[GOAL]
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
z_ne_zero : z ≠ 0
⊢ False
[PROOFSTEP]
rcases key with (key | key | key)
[GOAL]
case intro.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ False
[PROOFSTEP]
exact z_ne_zero (by rwa [key, self_eq_add_left] at h1 )
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ z = 0
[PROOFSTEP]
rwa [key, self_eq_add_left] at h1
[GOAL]
case intro.inr.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ False
[PROOFSTEP]
exact one_ne_zero (by rwa [key, self_eq_add_right] at h1 )
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ 1 = 0
[PROOFSTEP]
rwa [key, self_eq_add_right] at h1
[GOAL]
case intro.inr.inr
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ False
[PROOFSTEP]
exact z_ne_zero (pow_eq_zero (by rwa [key, add_self_eq_zero] at h2 ))
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ z ^ ?m.10353 = 0
[PROOFSTEP]
rwa [key, add_self_eq_zero] at h2
[GOAL]
n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
by_cases hn0 : n = 0
[GOAL]
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
[GOAL]
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)
[PROOFSTEP]
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by simp only [trinomial, C_neg, C_1]; ring
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
[PROOFSTEP]
simp only [trinomial, C_neg, C_1]
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ X ^ n - X - 1 = -1 * X ^ 0 + -1 * X ^ 1 + 1 * X ^ n
[PROOFSTEP]
ring
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
rw [hp]
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (trinomial 0 1 n (-1) (-1) 1)
[PROOFSTEP]
apply IsUnitTrinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ ∀ (z : ℂ),
    ¬(↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0 ∧ ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0)
[PROOFSTEP]
rintro z ⟨h1, h2⟩
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ False
[PROOFSTEP]
apply X_pow_sub_X_sub_one_irreducible_aux z
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h2 : ↑(aeval z) (trinomial 0 (n - 1 + 0) n ↑1 ↑(-1) ↑(-1)) = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
simp_rw [trinomial, aeval_add, aeval_mul, aeval_X_pow, aeval_C, Units.val_neg, Units.val_one, map_neg, map_one] at h1 h2
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
replace h1 : z ^ n = z + 1 := by linear_combination h1
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ n = z + 1
[PROOFSTEP]
linear_combination h1
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
h1 : z ^ n = z + 1
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
replace h2 := mul_eq_zero_of_left h2 z
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : z ^ n = z + 1
h2 : (1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n) * z = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
rw [add_mul, add_mul, add_zero, mul_assoc (-1 : ℂ), ← pow_succ', Nat.sub_add_cancel hn.le] at h2
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * z ^ n + -1 * z ^ n * z = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
rw [h1] at h2 ⊢
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 = z + 1 ∧ z + 1 + z ^ 2 = 0
[PROOFSTEP]
exact ⟨rfl, by linear_combination -h2⟩
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 + z ^ 2 = 0
[PROOFSTEP]
linear_combination -h2
[GOAL]
n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
by_cases hn0 : n = 0
[GOAL]
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
[GOAL]
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)
[PROOFSTEP]
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by simp only [trinomial, C_neg, C_1]; ring
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
[PROOFSTEP]
simp only [trinomial, C_neg, C_1]
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ X ^ n - X - 1 = -1 * X ^ 0 + -1 * X ^ 1 + 1 * X ^ n
[PROOFSTEP]
ring
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have h := (IsPrimitive.Int.irreducible_iff_irreducible_map_cast ?_).mp (X_pow_sub_X_sub_one_irreducible hn1)
[GOAL]
case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n - X - 1))
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one, Polynomial.map_X] at h
[GOAL]
case neg.refine_1
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ IsPrimitive (X ^ n - X - 1)
[PROOFSTEP]
exact hp.symm ▸ (trinomial_monic zero_lt_one hn).isPrimitive


[GOAL]
S : Type u
inst✝ : Semiring S
⊢ pochhammer S 1 = X
[PROOFSTEP]
simp [pochhammer]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S (n + 1) = X * comp (pochhammer S n) (X + 1)
[PROOFSTEP]
rw [pochhammer]
[GOAL]
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
⊢ map f (pochhammer S n) = pochhammer T n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
⊢ map f (pochhammer S Nat.zero) = pochhammer T Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
ih : map f (pochhammer S n) = pochhammer T n
⊢ map f (pochhammer S (Nat.succ n)) = pochhammer T (Nat.succ n)
[PROOFSTEP]
simp [ih, pochhammer_succ_left, map_comp]
[GOAL]
S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval k (pochhammer ℕ n)) = eval (↑k) (pochhammer S n)
[PROOFSTEP]
rw [← pochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S), eval₂_at_nat_cast, Nat.cast_id,
  eq_natCast]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ eval 0 (pochhammer S n) = if n = 0 then 1 else 0
[PROOFSTEP]
cases n
[GOAL]
case zero
S : Type u
inst✝ : Semiring S
⊢ eval 0 (pochhammer S Nat.zero) = if Nat.zero = 0 then 1 else 0
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u
inst✝ : Semiring S
n✝ : ℕ
⊢ eval 0 (pochhammer S (Nat.succ n✝)) = if Nat.succ n✝ = 0 then 1 else 0
[PROOFSTEP]
simp [X_mul, Nat.succ_ne_zero, pochhammer_succ_left]
[GOAL]
S : Type u
inst✝ : Semiring S
⊢ eval 0 (pochhammer S 0) = 1
[PROOFSTEP]
simp
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
h : n ≠ 0
⊢ eval 0 (pochhammer S n) = 0
[PROOFSTEP]
simp [pochhammer_eval_zero, h]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
[PROOFSTEP]
suffices h : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + (n : ℕ[X]))
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
h : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
[PROOFSTEP]
apply_fun Polynomial.map (algebraMap ℕ S) at h
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
h : map (algebraMap ℕ S) (pochhammer ℕ (n + 1)) = map (algebraMap ℕ S) (pochhammer ℕ n * (X + ↑n))
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
[PROOFSTEP]
simpa only [pochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X, Polynomial.map_nat_cast] using h
[GOAL]
case h
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case h.zero
S : Type u
inst✝ : Semiring S
⊢ pochhammer ℕ (Nat.zero + 1) = pochhammer ℕ Nat.zero * (X + ↑Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case h.succ
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
⊢ pochhammer ℕ (Nat.succ n + 1) = pochhammer ℕ (Nat.succ n) * (X + ↑(Nat.succ n))
[PROOFSTEP]
conv_lhs =>
  rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp, nat_cast_comp,
    add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
| pochhammer ℕ (Nat.succ n + 1)
[PROOFSTEP]
rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp, nat_cast_comp, add_assoc,
    add_comm (1 : ℕ[X]), ← Nat.cast_succ]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
| pochhammer ℕ (Nat.succ n + 1)
[PROOFSTEP]
rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp, nat_cast_comp, add_assoc,
    add_comm (1 : ℕ[X]), ← Nat.cast_succ]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
| pochhammer ℕ (Nat.succ n + 1)
[PROOFSTEP]
rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp, nat_cast_comp, add_assoc,
  add_comm (1 : ℕ[X]), ← Nat.cast_succ]
[GOAL]
S✝ : Type u
inst✝¹ : Semiring S✝
S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (pochhammer S (n + 1)) = eval k (pochhammer S n) * (k + ↑n)
[PROOFSTEP]
rw [pochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_nat_cast, eval_C_mul, Nat.cast_comm, ←
  mul_add]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer S (n + 1)) (X + 1) = pochhammer S (n + 1) + (n + 1) • comp (pochhammer S n) (X + 1)
[PROOFSTEP]
suffices (pochhammer ℕ (n + 1)).comp (X + 1) = pochhammer ℕ (n + 1) + (n + 1) * (pochhammer ℕ n).comp (X + 1) by
  simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
this : comp (pochhammer ℕ (n + 1)) (X + 1) = pochhammer ℕ (n + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
⊢ comp (pochhammer S (n + 1)) (X + 1) = pochhammer S (n + 1) + (n + 1) • comp (pochhammer S n) (X + 1)
[PROOFSTEP]
simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = pochhammer ℕ (n + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
[PROOFSTEP]
nth_rw 2 [pochhammer_succ_left]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = X * comp (pochhammer ℕ n) (X + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
[PROOFSTEP]
rw [← add_mul, pochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, nat_cast_comp, add_comm, ← add_assoc]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (↑n + X + 1) * comp (pochhammer ℕ n) (X + 1) = (X + (↑n + 1)) * comp (pochhammer ℕ n) (X + 1)
[PROOFSTEP]
ring
[GOAL]
S : Type u
inst✝ : Semiring S
p q : S[X]
n : ℕ
⊢ comp (p * (X + ↑n)) q = comp p q * (q + ↑n)
[PROOFSTEP]
rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, nat_cast_mul_comp, Nat.cast_comm, mul_add]
[GOAL]
S : Type u
inst✝ : Semiring S
n m : ℕ
⊢ pochhammer S n * comp (pochhammer S m) (X + ↑n) = pochhammer S (n + m)
[PROOFSTEP]
induction' m with m ih
[GOAL]
case zero
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S n * comp (pochhammer S Nat.zero) (X + ↑n) = pochhammer S (n + Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : pochhammer S n * comp (pochhammer S m) (X + ↑n) = pochhammer S (n + m)
⊢ pochhammer S n * comp (pochhammer S (Nat.succ m)) (X + ↑n) = pochhammer S (n + Nat.succ m)
[PROOFSTEP]
rw [pochhammer_succ_right, Polynomial.mul_X_add_nat_cast_comp, ← mul_assoc, ih, Nat.succ_eq_add_one, ← add_assoc,
  pochhammer_succ_right, Nat.cast_add, add_assoc]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ eval (n + 1) (pochhammer ℕ 0) = Nat.ascFactorial n 0
[PROOFSTEP]
rw [pochhammer_zero, eval_one, Nat.ascFactorial_zero]
[GOAL]
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ eval (n + 1) (pochhammer ℕ (t + 1)) = Nat.ascFactorial n (t + 1)
[PROOFSTEP]
rw [pochhammer_succ_right, eval_mul, pochhammer_nat_eq_ascFactorial n t]
[GOAL]
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ Nat.ascFactorial n t * eval (n + 1) (X + ↑t) = Nat.ascFactorial n (t + 1)
[PROOFSTEP]
simp only [eval_add, eval_X, eval_nat_cast, Nat.cast_id]
[GOAL]
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ Nat.ascFactorial n t * (n + 1 + t) = Nat.ascFactorial n (t + 1)
[PROOFSTEP]
rw [Nat.ascFactorial_succ, add_right_comm, mul_comm]
[GOAL]
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ b) = Nat.descFactorial (a + b - 1) b
[PROOFSTEP]
cases' b with b
[GOAL]
case zero
S : Type u
inst✝ : Semiring S
a : ℕ
⊢ eval a (pochhammer ℕ Nat.zero) = Nat.descFactorial (a + Nat.zero - 1) Nat.zero
[PROOFSTEP]
rw [Nat.descFactorial_zero, pochhammer_zero, Polynomial.eval_one]
[GOAL]
case succ
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (a + Nat.succ b - 1) (Nat.succ b)
[PROOFSTEP]
rw [Nat.add_succ, Nat.succ_sub_succ, tsub_zero]
[GOAL]
case succ
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (a + b) (Nat.succ b)
[PROOFSTEP]
cases a
[GOAL]
case succ.zero
S : Type u
inst✝ : Semiring S
b : ℕ
⊢ eval Nat.zero (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (Nat.zero + b) (Nat.succ b)
[PROOFSTEP]
simp only [Nat.zero_eq, ne_eq, Nat.succ_ne_zero, not_false_iff, pochhammer_ne_zero_eval_zero, zero_add,
  Nat.descFactorial_succ, le_refl, tsub_eq_zero_of_le, zero_mul]
[GOAL]
case succ.succ
S : Type u
inst✝ : Semiring S
b n✝ : ℕ
⊢ eval (Nat.succ n✝) (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (Nat.succ n✝ + b) (Nat.succ b)
[PROOFSTEP]
rw [Nat.succ_add, ← Nat.add_succ, Nat.add_descFactorial_eq_ascFactorial, pochhammer_nat_eq_ascFactorial]
[GOAL]
S : Type u_1
inst✝ : StrictOrderedSemiring S
n : ℕ
s : S
h : 0 < s
⊢ 0 < eval s (pochhammer S n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < eval s (pochhammer S Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, pochhammer_zero, eval_one]
[GOAL]
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (pochhammer S n)
⊢ 0 < eval s (pochhammer S (Nat.succ n))
[PROOFSTEP]
rw [pochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_nat_cast_mul, eval_mul_X, Nat.cast_comm, ← mul_add]
[GOAL]
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (pochhammer S n)
⊢ 0 < eval s (pochhammer S n) * (s + ↑n)
[PROOFSTEP]
exact mul_pos ih (lt_of_lt_of_le h ((le_add_iff_nonneg_right _).mpr (Nat.cast_nonneg n)))
[GOAL]
S✝ : Type u_1
inst✝¹ : Semiring S✝
r n✝ : ℕ
S : Type u_2
inst✝ : Semiring S
n : ℕ
⊢ eval 1 (pochhammer S n) = ↑n !
[PROOFSTEP]
rw_mod_cast [pochhammer_nat_eq_ascFactorial, Nat.zero_ascFactorial]
[GOAL]
S✝ : Type u_1
inst✝¹ : Semiring S✝
r✝ n✝ : ℕ
S : Type u_2
inst✝ : Semiring S
r n : ℕ
⊢ ↑r ! * eval (↑r + 1) (pochhammer S n) = ↑(r + n)!
[PROOFSTEP]
rw_mod_cast [pochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
[GOAL]
S : Type u_1
inst✝ : Semiring S
r✝ n r : ℕ
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
[PROOFSTEP]
by_cases h : r = 0
[GOAL]
case pos
S : Type u_1
inst✝ : Semiring S
r✝ n r : ℕ
h : r = 0
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
[PROOFSTEP]
simp only [h, zero_mul, zero_add]
[GOAL]
case neg
S : Type u_1
inst✝ : Semiring S
r✝ n r : ℕ
h : ¬r = 0
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
[PROOFSTEP]
simp only [pochhammer_eval_zero, zero_mul, if_neg h, mul_zero]
[GOAL]
S : Type u_1
inst✝ : Semiring S
r✝ n r k : ℕ
⊢ (k + 1) * eval (k + 1 + 1) (pochhammer ℕ r) = (k + 1 + r) * eval (k + 1) (pochhammer ℕ r)
[PROOFSTEP]
simp only [pochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial, add_right_comm]
[GOAL]
S : Type u_1
inst✝ : Semiring S
r✝ n✝ r n : ℕ
⊢ ↑n * eval (↑n + 1) (pochhammer S r) = (↑n + ↑r) * eval (↑n) (pochhammer S r)
[PROOFSTEP]
exact_mod_cast congr_arg Nat.cast (pochhammer_nat_eval_succ r n)