[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
i : ℕ
⊢ coeff (scaleRoots p s) i = coeff p i * s ^ (natDegree p - i)
[PROOFSTEP]
simp (config := { contextual := true }) [scaleRoots, coeff_monomial]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ coeff (scaleRoots p s) (natDegree p) = leadingCoeff p
[PROOFSTEP]
rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
s : R
⊢ scaleRoots 0 s = 0
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
s : R
n✝ : ℕ
⊢ coeff (scaleRoots 0 s) n✝ = coeff 0 n✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
⊢ scaleRoots p s ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
h : scaleRoots p s = 0
⊢ False
[PROOFSTEP]
have : p.coeff p.natDegree ≠ 0 := mt leadingCoeff_eq_zero.mp hp
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
h : scaleRoots p s = 0
this : coeff p (natDegree p) ≠ 0
⊢ False
[PROOFSTEP]
have : (scaleRoots p s).coeff p.natDegree = 0 := congr_fun (congr_arg (coeff : R[X] → ℕ → R) h) p.natDegree
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
h : scaleRoots p s = 0
this✝ : coeff p (natDegree p) ≠ 0
this : coeff (scaleRoots p s) (natDegree p) = 0
⊢ False
[PROOFSTEP]
rw [coeff_scaleRoots_natDegree] at this
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
h : scaleRoots p s = 0
this✝ : coeff p (natDegree p) ≠ 0
this : leadingCoeff p = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ support (scaleRoots p s) ≤ support p
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
a✝ : ℕ
⊢ a✝ ∈ support (scaleRoots p s) → a✝ ∈ support p
[PROOFSTEP]
simpa using left_ne_zero_of_mul
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
⊢ support p ≤ support (scaleRoots p s)
[PROOFSTEP]
intro i
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ i ∈ support p → i ∈ support (scaleRoots p s)
[PROOFSTEP]
simp only [coeff_scaleRoots, Polynomial.mem_support_iff]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ coeff p i ≠ 0 → coeff p i * s ^ (natDegree p - i) ≠ 0
[PROOFSTEP]
intro p_ne_zero ps_zero
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : coeff p i ≠ 0
ps_zero : coeff p i * s ^ (natDegree p - i) = 0
⊢ False
[PROOFSTEP]
have := pow_mem hs (p.natDegree - i) _ ps_zero
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : coeff p i ≠ 0
ps_zero : coeff p i * s ^ (natDegree p - i) = 0
this : coeff p i = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ degree (scaleRoots p s) = degree p
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
⊢ degree (scaleRoots p s) = degree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ degree (scaleRoots p s) = degree p
[PROOFSTEP]
rw [hp, zero_scaleRoots]
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ degree (scaleRoots p s) = degree p
[PROOFSTEP]
refine' le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree _)
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ coeff (scaleRoots p s) (natDegree p) ≠ 0
[PROOFSTEP]
rw [coeff_scaleRoots_natDegree]
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ leadingCoeff p ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
h : leadingCoeff p = 0
⊢ False
[PROOFSTEP]
have := leadingCoeff_eq_zero.mp h
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this✝ : (a : Prop) → Decidable a
hp : ¬p = 0
h : leadingCoeff p = 0
this : p = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ natDegree (scaleRoots p s) = natDegree p
[PROOFSTEP]
simp only [natDegree, degree_scaleRoots]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ Monic (scaleRoots p s) ↔ Monic p
[PROOFSTEP]
simp only [Monic, leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : ↑f (leadingCoeff p) ≠ 0
⊢ map f (scaleRoots p x) = scaleRoots (map f p) (↑f x)
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : ↑f (leadingCoeff p) ≠ 0
n✝ : ℕ
⊢ coeff (map f (scaleRoots p x)) n✝ = coeff (scaleRoots (map f p) (↑f x)) n✝
[PROOFSTEP]
simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
⊢ eval₂ f (↑f s * r) (scaleRoots p s) =
    ∑ i in support (scaleRoots p s), ↑f (coeff p i * s ^ (natDegree p - i)) * (↑f s * r) ^ i
[PROOFSTEP]
simp [eval₂_eq_sum, sum_def]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
_hi : i ∈ support p
hi' : ¬i ∈ support (scaleRoots p s)
⊢ ↑f (coeff p i * s ^ (natDegree p - i)) * (↑f s * r) ^ i = 0
[PROOFSTEP]
let this : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
_hi : i ∈ support p
hi' : ¬i ∈ support (scaleRoots p s)
⊢ coeff p i * s ^ (natDegree p - i) = 0
[PROOFSTEP]
simpa using hi'
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
_hi : i ∈ support p
hi' : ¬i ∈ support (scaleRoots p s)
this : coeff p i * s ^ (natDegree p - i) = 0 :=
  Eq.mp
    (Eq.trans
      (congrArg Not
        (Eq.trans Mathlib.Data.Polynomial.Basic._auxLemma.17 (congrFun (congrArg Ne (coeff_scaleRoots p s i)) 0)))
      Mathlib.Logic.Basic._auxLemma.9)
    hi'
⊢ ↑f (coeff p i * s ^ (natDegree p - i)) * (↑f s * r) ^ i = 0
[PROOFSTEP]
simp [this]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
_hi : i ∈ support p
⊢ ↑f (coeff p i * s ^ (natDegree p - i)) * (↑f s * r) ^ i = ↑f (coeff p i) * ↑f s ^ (natDegree p - i + i) * r ^ i
[PROOFSTEP]
simp_rw [f.map_mul, f.map_pow, pow_add, mul_pow, mul_assoc]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
hi : i ∈ support p
⊢ ↑f (coeff p i) * ↑f s ^ (natDegree p - i + i) * r ^ i = ↑f s ^ natDegree p * (↑f (coeff p i) * r ^ i)
[PROOFSTEP]
rw [mul_assoc, mul_left_comm, tsub_add_cancel_of_le]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
hi : i ∈ support p
⊢ i ≤ natDegree p
[PROOFSTEP]
exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
⊢ ↑f s ^ natDegree p * ∑ i in support p, ↑f (coeff p i) * r ^ i = ↑f s ^ natDegree p * eval₂ f r p
[PROOFSTEP]
simp [eval₂_eq_sum, sum_def]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ eval₂ f (↑f s * r) (scaleRoots p s) = 0
[PROOFSTEP]
rw [scaleRoots_eval₂_mul, hr, mul_zero]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ↑f
r s : S
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors S
⊢ eval₂ f (↑f r) (scaleRoots p s) = 0
[PROOFSTEP]
nontriviality S using Subsingleton.eq_zero
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ↑f
r s : S
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors S
✝ : Nontrivial S
⊢ eval₂ f (↑f r) (scaleRoots p s) = 0
[PROOFSTEP]
convert @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr
[GOAL]
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ↑f
r s : S
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors S
✝ : Nontrivial S
⊢ ↑f r = ↑f s * (↑f r / ↑f s)
[PROOFSTEP]
rw [← mul_div_assoc, mul_comm, mul_div_cancel]
[GOAL]
case h.e'_2.h.e'_6.h
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ↑f
r s : S
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors S
✝ : Nontrivial S
⊢ ↑f s ≠ 0
[PROOFSTEP]
exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs


[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ ↑(aeval x) (map (algebraMap R A) p) = ↑(aeval x) p
[PROOFSTEP]
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
⊢ ↑(aeval (↑(algebraMap A B) x)) p = ↑(algebraMap A B) (↑(aeval x) p)
[PROOFSTEP]
rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Nontrivial B
x : A
p : R[X]
⊢ ↑(aeval (↑(algebraMap A B) x)) p = 0 ↔ ↑(aeval x) p = 0
[PROOFSTEP]
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero, iff_false_intro (one_ne_zero' B),
  or_false_iff]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ↑(algebraMap A B)
⊢ ↑(aeval (↑(algebraMap A B) x)) p = 0 ↔ ↑(aeval x) p = 0
[PROOFSTEP]
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]


[GOAL]
n : ℕ
x : ℝ
⊢ deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
n : ℕ
x : ℝ
⊢ deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
induction' n with n ih generalizing x
[GOAL]
case zero
x✝ x : ℝ
⊢ deriv^[Nat.zero] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ Nat.zero * (↑(aeval x) (hermite Nat.zero) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]
[GOAL]
case succ
x✝ : ℝ
n : ℕ
ih :
  ∀ (x : ℝ),
    deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
x : ℝ
⊢ deriv^[Nat.succ n] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ Nat.succ n * (↑(aeval x) (hermite (Nat.succ n)) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
replace ih : deriv^[n] _ = _ := _root_.funext ih
[GOAL]
case succ
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ deriv^[Nat.succ n] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ Nat.succ n * (↑(aeval x) (hermite (Nat.succ n)) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
have deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2)) := by
  rw [deriv_exp (by simp)]; simp;
  ring
    -- Porting note: was `simp [mul_comm, ← neg_mul]`
[GOAL]
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
rw [deriv_exp (by simp)]
[GOAL]
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ DifferentiableAt ℝ (fun y => -(y ^ 2 / 2)) x
[PROOFSTEP]
simp
[GOAL]
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ Real.exp (-(x ^ 2 / 2)) * deriv (fun y => -(y ^ 2 / 2)) x = -x * Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
simp
[GOAL]
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ Real.exp (-(x ^ 2 / 2)) * (2 * x / 2) = x * Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
ring
  -- Porting note: was `simp [mul_comm, ← neg_mul]`
[GOAL]
case succ
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ deriv^[Nat.succ n] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ Nat.succ n * (↑(aeval x) (hermite (Nat.succ n)) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_mul, pow_succ (-1 : ℝ), deriv_gaussian, hermite_succ,
  map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]
[GOAL]
case succ
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ (-1) ^ n *
      (↑(aeval x) (↑derivative (hermite n)) * Real.exp (-(x ^ 2 / 2)) +
        ↑(aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    -1 * (-1) ^ n * ((x * ↑(aeval x) (hermite n) - ↑(aeval x) (↑derivative (hermite n))) * Real.exp (-(x ^ 2 / 2)))
case succ.hc
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => ↑(aeval x) (hermite n)) x
case succ.hd
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => Real.exp (-(x ^ 2 / 2))) x
[PROOFSTEP]
ring
[GOAL]
case succ.hc
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => ↑(aeval x) (hermite n)) x
[PROOFSTEP]
apply Polynomial.differentiable_aeval
[GOAL]
case succ.hd
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => Real.exp (-(x ^ 2 / 2))) x
[PROOFSTEP]
apply DifferentiableAt.exp
[GOAL]
case succ.hd.hc
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => -(x ^ 2 / 2)) x
[PROOFSTEP]
simp
  -- Porting note: was just `simp`
[GOAL]
n : ℕ
x : ℝ
⊢ ↑(aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
rw [deriv_gaussian_eq_hermite_mul_gaussian]
[GOAL]
n : ℕ
x : ℝ
⊢ ↑(aeval x) (hermite n) =
    (-1) ^ n * ((-1) ^ n * ↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))) / Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
field_simp [Real.exp_ne_zero]
[GOAL]
n : ℕ
x : ℝ
⊢ ↑(aeval x) (hermite n) * Real.exp (-x ^ 2 / 2) =
    (-1) ^ n * ((-1) ^ n * ↑(aeval x) (hermite n) * Real.exp (-x ^ 2 / 2))
[PROOFSTEP]
rw [← @smul_eq_mul ℝ _ ((-1) ^ n), ← inv_smul_eq_iff₀, mul_assoc, smul_eq_mul, ← inv_pow, ← neg_inv, inv_one]
[GOAL]
case ha
n : ℕ
x : ℝ
⊢ (-1) ^ n ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ (by norm_num)
[GOAL]
n : ℕ
x : ℝ
⊢ -1 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
x : ℝ
⊢ ↑(aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)
[PROOFSTEP]
rw [hermite_eq_deriv_gaussian, Real.exp_neg]
[GOAL]
n : ℕ
x : ℝ
⊢ (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / (Real.exp (x ^ 2 / 2))⁻¹ =
    (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)
[PROOFSTEP]
field_simp [Real.exp_ne_zero]


[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
⊢ integralNormalization 0 = 0
[PROOFSTEP]
simp [integralNormalization]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ coeff (integralNormalization f) i = if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
[PROOFSTEP]
have : f.coeff i = 0 → f.degree ≠ i := fun hc hd => coeff_ne_zero_of_eq_degree hd hc
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
this : coeff f i = 0 → degree f ≠ ↑i
⊢ coeff (integralNormalization f) i = if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
[PROOFSTEP]
simp (config := { contextual := true }) [integralNormalization, coeff_monomial, this, mem_support_iff]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
⊢ support (integralNormalization f) ⊆ support f
[PROOFSTEP]
intro
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
a✝ : ℕ
⊢ a✝ ∈ support (integralNormalization f) → a✝ ∈ support f
[PROOFSTEP]
simp (config := { contextual := true }) [integralNormalization, coeff_monomial, mem_support_iff]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
hi : degree f = ↑i
⊢ coeff (integralNormalization f) i = 1
[PROOFSTEP]
rw [integralNormalization_coeff, if_pos hi]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
hi : degree f ≠ ↑i
⊢ coeff (integralNormalization f) i = coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
[PROOFSTEP]
rw [integralNormalization_coeff, if_neg hi]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
⊢ support (integralNormalization f) = support f
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : f = 0
⊢ support (integralNormalization f) = support f
[PROOFSTEP]
simp [hf]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
⊢ support (integralNormalization f) = support f
[PROOFSTEP]
ext i
[GOAL]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ i ∈ support (integralNormalization f) ↔ i ∈ support f
[PROOFSTEP]
refine' ⟨fun h => integralNormalization_support h, _⟩
[GOAL]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ i ∈ support f → i ∈ support (integralNormalization f)
[PROOFSTEP]
simp only [integralNormalization_coeff, mem_support_iff]
[GOAL]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ coeff f i ≠ 0 → (if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)) ≠ 0
[PROOFSTEP]
intro hfi
[GOAL]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
hfi : coeff f i ≠ 0
⊢ (if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)) ≠ 0
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
hfi : coeff f i ≠ 0
hi : degree f = ↑i
⊢ 1 ≠ 0
[PROOFSTEP]
simp [hfi, hi, pow_ne_zero _ (leadingCoeff_ne_zero.mpr hf)]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
hfi : coeff f i ≠ 0
hi : ¬degree f = ↑i
⊢ coeff f i * leadingCoeff f ^ (natDegree f - 1 - i) ≠ 0
[PROOFSTEP]
simp [hfi, hi, pow_ne_zero _ (leadingCoeff_ne_zero.mpr hf)]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ eval₂ f (z * ↑f (leadingCoeff p)) (integralNormalization p) =
    ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i
[PROOFSTEP]
rw [eval₂_eq_sum, sum_def, support_integralNormalization]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ n in support p, ↑f (coeff (integralNormalization p) n) * (z * ↑f (leadingCoeff p)) ^ n =
    ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i
[PROOFSTEP]
simp only [mul_comm z, mul_pow, mul_assoc, RingHom.map_pow, RingHom.map_mul]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ x in support p, ↑f (coeff (integralNormalization p) x) * (↑f (leadingCoeff p) ^ x * z ^ x) =
    ∑ x in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑x) * (↑f (leadingCoeff p) ^ ↑x * z ^ ↑x)
[PROOFSTEP]
exact Finset.sum_attach.symm
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : p = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
[PROOFSTEP]
have one_le_deg : 1 ≤ natDegree p := Nat.succ_le_of_lt (natDegree_pos_of_eval₂_root hp f hz inj)
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
[PROOFSTEP]
congr with i
[GOAL]
case neg.e_f.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
⊢ ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
[PROOFSTEP]
congr 2
[GOAL]
case neg.e_f.h.e_a.h.e_6.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
[PROOFSTEP]
by_cases hi : i.1 = natDegree p
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ↑i = natDegree p
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
[PROOFSTEP]
rw [hi, integralNormalization_coeff_degree, one_mul, leadingCoeff, ← pow_succ, tsub_add_cancel_of_le one_le_deg]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ↑i = natDegree p
⊢ degree p = ↑(natDegree p)
[PROOFSTEP]
exact degree_eq_natDegree hp
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ¬↑i = natDegree p
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
[PROOFSTEP]
have : i.1 ≤ p.natDegree - 1 := Nat.le_pred_of_lt (lt_of_le_of_ne (le_natDegree_of_ne_zero (mem_support_iff.mp i.2)) hi)
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ¬↑i = natDegree p
this : ↑i ≤ natDegree p - 1
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
[PROOFSTEP]
rw [integralNormalization_coeff_ne_natDegree hi, mul_assoc, ← pow_add, tsub_add_cancel_of_le this]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * eval₂ f z p
[PROOFSTEP]
simp_rw [eval₂_eq_sum, sum_def, fun i => mul_comm (coeff p i), RingHom.map_mul, RingHom.map_pow, mul_assoc, ←
  Finset.mul_sum]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ↑f (leadingCoeff p) ^ (natDegree p - 1) * ∑ x in Finset.attach (support p), ↑f (coeff p ↑x) * z ^ ↑x =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * ∑ n in support p, ↑f (coeff p n) * z ^ n
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ x in Finset.attach (support p), ↑f (coeff p ↑x) * z ^ ↑x = ∑ n in support p, ↑f (coeff p n) * z ^ n
[PROOFSTEP]
exact @Finset.sum_attach _ _ p.support _ fun i => f (p.coeff i) * z ^ i
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ↑f (leadingCoeff p) ^ (natDegree p - 1) * eval₂ f z p = 0
[PROOFSTEP]
rw [hz, mul_zero]


[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
⊢ ζ ^ n = 1
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
R : Type u_1
inst✝ : CommRing R
ζ : R
i : ℕ
h : IsRoot (cyclotomic i R) ζ
hi : i ∈ Nat.divisors 0
⊢ ζ ^ 0 = 1
[PROOFSTEP]
exact pow_zero _
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
⊢ ζ ^ n = 1
[PROOFSTEP]
have := congr_arg (eval ζ) (prod_cyclotomic_eq_X_pow_sub_one hn R).symm
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : eval ζ (X ^ n - 1) = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ ζ ^ n = 1
[PROOFSTEP]
rw [eval_sub, eval_pow, eval_X, eval_one] at this
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ ζ ^ n = 1
[PROOFSTEP]
convert eq_add_of_sub_eq' this
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ 1 = 1 + eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
[PROOFSTEP]
convert (add_zero (M := R) _).symm
[GOAL]
case h.e'_3.h.e'_6
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ eval ζ (∏ i in Nat.divisors n, cyclotomic i R) = 0
[PROOFSTEP]
apply eval_eq_zero_of_dvd_of_eval_eq_zero _ h
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ cyclotomic i R ∣ ∏ i in Nat.divisors n, cyclotomic i R
[PROOFSTEP]
exact Finset.dvd_prod_of_mem _ hi
[GOAL]
R✝ : Type u_1
inst✝³ : CommRing R✝
n : ℕ
inst✝² : IsDomain R✝
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ ζ ^ n = 1 ↔ ∃ i, i ∈ Nat.divisors n ∧ IsRoot (cyclotomic i R) ζ
[PROOFSTEP]
rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ← prod_cyclotomic_eq_X_pow_sub_one h,
  isRoot_prod]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ IsRoot (cyclotomic n R) μ
[PROOFSTEP]
rw [← mem_roots (cyclotomic_ne_zero n R), cyclotomic_eq_prod_X_sub_primitiveRoots h, roots_prod_X_sub_C, ←
  Finset.mem_def]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ μ ∈ primitiveRoots n R
[PROOFSTEP]
rwa [← mem_primitiveRoots hpos] at h
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
⊢ IsRoot (cyclotomic n K) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
have hnpos : 0 < n := (NeZero.of_neZero_natCast K).out.bot_lt
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
⊢ IsRoot (cyclotomic n K) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
refine' ⟨fun hμ => _, IsPrimitiveRoot.isRoot_cyclotomic hnpos⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
⊢ IsPrimitiveRoot μ n
[PROOFSTEP]
have hμn : μ ^ n = 1 := by
  rw [isRoot_of_unity_iff hnpos _]
  exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
⊢ μ ^ n = 1
[PROOFSTEP]
rw [isRoot_of_unity_iff hnpos _]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
⊢ ∃ i, i ∈ Nat.divisors n ∧ IsRoot (cyclotomic i K) μ
[PROOFSTEP]
exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
⊢ IsPrimitiveRoot μ n
[PROOFSTEP]
by_contra hnμ
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ False
[PROOFSTEP]
have ho : 0 < orderOf μ := by
  apply orderOf_pos'
  rw [isOfFinOrder_iff_pow_eq_one]
  exact ⟨n, hnpos, hμn⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ 0 < orderOf μ
[PROOFSTEP]
apply orderOf_pos'
[GOAL]
case h
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ IsOfFinOrder μ
[PROOFSTEP]
rw [isOfFinOrder_iff_pow_eq_one]
[GOAL]
case h
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ ∃ n, 0 < n ∧ μ ^ n = 1
[PROOFSTEP]
exact ⟨n, hnpos, hμn⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
⊢ False
[PROOFSTEP]
have := pow_orderOf_eq_one μ
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : μ ^ orderOf μ = 1
⊢ False
[PROOFSTEP]
rw [isRoot_of_unity_iff ho] at this
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : ∃ i, i ∈ Nat.divisors (orderOf μ) ∧ IsRoot (cyclotomic i K) μ
⊢ False
[PROOFSTEP]
obtain ⟨i, hio, hiμ⟩ := this
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∈ Nat.divisors (orderOf μ)
hiμ : IsRoot (cyclotomic i K) μ
⊢ False
[PROOFSTEP]
replace hio := Nat.dvd_of_mem_divisors hio
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
[PROOFSTEP]
rw [IsPrimitiveRoot.not_iff] at hnμ
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one] at hμn
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
[PROOFSTEP]
have key : i < n := (Nat.le_of_dvd ho hio).trans_lt ((Nat.le_of_dvd hnpos hμn).lt_of_ne hnμ)
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
key : i < n
⊢ False
[PROOFSTEP]
have key' : i ∣ n := hio.trans hμn
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False
[PROOFSTEP]
rw [← Polynomial.dvd_iff_isRoot] at hμ hiμ
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - ↑C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - ↑C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False
[PROOFSTEP]
have hni : { i, n } ⊆ n.divisors := by simpa [Finset.insert_subset_iff, key'] using hnpos.ne'
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - ↑C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - ↑C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ {i, n} ⊆ Nat.divisors n
[PROOFSTEP]
simpa [Finset.insert_subset_iff, key'] using hnpos.ne'
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - ↑C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - ↑C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
⊢ False
[PROOFSTEP]
obtain ⟨k, hk⟩ := hiμ
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - ↑C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
⊢ False
[PROOFSTEP]
obtain ⟨j, hj⟩ := hμ
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
⊢ False
[PROOFSTEP]
have := prod_cyclotomic_eq_X_pow_sub_one hnpos K
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : ∏ i in Nat.divisors n, cyclotomic i K = X ^ n - 1
⊢ False
[PROOFSTEP]
rw [← Finset.prod_sdiff hni, Finset.prod_pair key.ne, hk, hj] at this
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
⊢ False
[PROOFSTEP]
have hn := (X_pow_sub_one_separable_iff.mpr <| NeZero.natCast_ne n K).squarefree
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn : Squarefree (X ^ n - 1)
⊢ False
[PROOFSTEP]
rw [← this, Squarefree] at hn
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn :
  ∀ (x : K[X]),
    x * x ∣ (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) → IsUnit x
⊢ False
[PROOFSTEP]
contrapose! hn
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn : ¬False
⊢ ∃ x, x * x ∣ (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) ∧ ¬IsUnit x
[PROOFSTEP]
refine' ⟨X - C μ, ⟨(∏ x in n.divisors \ { i, n }, cyclotomic x K) * k * j, by ring⟩, _⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn : ¬False
⊢ (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) =
    (X - ↑C μ) * (X - ↑C μ) * ((∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * k * j)
[PROOFSTEP]
ring
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn : ¬False
⊢ ¬IsUnit (X - ↑C μ)
[PROOFSTEP]
simp [Polynomial.isUnit_iff_degree_eq_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
have hf : Function.Injective _ := IsFractionRing.injective R (FractionRing R)
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ↑(algebraMap R (FractionRing R))
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
haveI : NeZero (n : FractionRing R) := NeZero.nat_of_injective hf
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ↑(algebraMap R (FractionRing R))
this : NeZero ↑n
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ← isRoot_cyclotomic_iff']
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ Multiset.Nodup (roots (cyclotomic n R))
[PROOFSTEP]
obtain h | ⟨ζ, hζ⟩ := (cyclotomic n R).roots.empty_or_exists_mem
[GOAL]
case inl
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
h : roots (cyclotomic n R) = 0
⊢ Multiset.Nodup (roots (cyclotomic n R))
[PROOFSTEP]
exact h.symm ▸ Multiset.nodup_zero
[GOAL]
case inr.intro
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : ζ ∈ roots (cyclotomic n R)
⊢ Multiset.Nodup (roots (cyclotomic n R))
[PROOFSTEP]
rw [mem_roots <| cyclotomic_ne_zero n R, isRoot_cyclotomic_iff] at hζ
[GOAL]
case inr.intro
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ Multiset.Nodup (roots (cyclotomic n R))
[PROOFSTEP]
refine'
  Multiset.nodup_of_le
    (roots.le_of_dvd (X_pow_sub_C_ne_zero (NeZero.pos_of_neZero_natCast R) 1) <| cyclotomic.dvd_X_pow_sub_one n R)
    hζ.nthRoots_nodup
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ { val := roots (cyclotomic n R), nodup := (_ : Multiset.Nodup (roots (cyclotomic n R))) } = primitiveRoots n R
[PROOFSTEP]
ext a
[GOAL]
case a
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := roots (cyclotomic n R), nodup := (_ : Multiset.Nodup (roots (cyclotomic n R))) } ↔ a ∈ primitiveRoots n R
[PROOFSTEP]
simp only [mem_primitiveRoots, NeZero.pos_of_neZero_natCast R]
[GOAL]
case a
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := roots (cyclotomic n R), nodup := (_ : Multiset.Nodup (roots (cyclotomic n R))) } ↔ IsPrimitiveRoot a n
[PROOFSTEP]
convert isRoot_cyclotomic_iff (n := n) (μ := a)
[GOAL]
case h.e'_1.a
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := roots (cyclotomic n R), nodup := (_ : Multiset.Nodup (roots (cyclotomic n R))) } ↔
    IsRoot (cyclotomic n R) a
[PROOFSTEP]
simp [cyclotomic_ne_zero n R]
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ roots (cyclotomic n R) = (primitiveRoots n R).val
[PROOFSTEP]
rw [← cyclotomic.roots_to_finset_eq_primitiveRoots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
⊢ Function.Injective fun n => cyclotomic n R
[PROOFSTEP]
intro n m hnm
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : (fun n => cyclotomic n R) n = (fun n => cyclotomic n R) m
⊢ n = m
[PROOFSTEP]
simp only at hnm
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
⊢ n = m
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hzero)
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : cyclotomic 0 R = cyclotomic m R
⊢ 0 = m
[PROOFSTEP]
rw [cyclotomic_zero] at hnm
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : 1 = cyclotomic m R
⊢ 0 = m
[PROOFSTEP]
replace hnm := congr_arg natDegree hnm
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : natDegree 1 = natDegree (cyclotomic m R)
⊢ 0 = m
[PROOFSTEP]
rw [natDegree_one, natDegree_cyclotomic] at hnm
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : 0 = Nat.totient m
⊢ 0 = m
[PROOFSTEP]
by_contra h
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : 0 = Nat.totient m
h : ¬0 = m
⊢ False
[PROOFSTEP]
exact (Nat.totient_pos (zero_lt_iff.2 (Ne.symm h))).ne hnm
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
hzero : n ≠ 0
⊢ n = m
[PROOFSTEP]
haveI := NeZero.mk hzero
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
hzero : n ≠ 0
this : NeZero n
⊢ n = m
[PROOFSTEP]
rw [← map_cyclotomic_int _ R, ← map_cyclotomic_int _ R] at hnm
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : map (Int.castRingHom R) (cyclotomic n ℤ) = map (Int.castRingHom R) (cyclotomic m ℤ)
hzero : n ≠ 0
this : NeZero n
⊢ n = m
[PROOFSTEP]
replace hnm := map_injective (Int.castRingHom R) Int.cast_injective hnm
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℤ = cyclotomic m ℤ
⊢ n = m
[PROOFSTEP]
replace hnm := congr_arg (map (Int.castRingHom ℂ)) hnm
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : map (Int.castRingHom ℂ) (cyclotomic n ℤ) = map (Int.castRingHom ℂ) (cyclotomic m ℤ)
⊢ n = m
[PROOFSTEP]
rw [map_cyclotomic_int, map_cyclotomic_int] at hnm
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
⊢ n = m
[PROOFSTEP]
have hprim := Complex.isPrimitiveRoot_exp _ hzero
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ n = m
[PROOFSTEP]
have hroot := isRoot_cyclotomic_iff (R := ℂ).2 hprim
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsRoot (cyclotomic n ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
⊢ n = m
[PROOFSTEP]
rw [hnm] at hroot
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
⊢ n = m
[PROOFSTEP]
haveI hmzero : NeZero m := ⟨fun h => by simp [h] at hroot ⟩
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
h : m = 0
⊢ False
[PROOFSTEP]
simp [h] at hroot
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
hmzero : NeZero m
⊢ n = m
[PROOFSTEP]
rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) m
hmzero : NeZero m
⊢ n = m
[PROOFSTEP]
replace hprim := hprim.eq_orderOf
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hroot : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) m
hmzero : NeZero m
hprim : n = orderOf (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
⊢ n = m
[PROOFSTEP]
rwa [← IsPrimitiveRoot.eq_orderOf hroot] at hprim
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ minpoly ℤ μ ∣ cyclotomic n ℤ
[PROOFSTEP]
apply minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos)
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ ↑(aeval μ) (cyclotomic n ℤ) = 0
[PROOFSTEP]
simpa [aeval_def, eval₂_eq_eval_map, IsRoot.def] using h.isRoot_cyclotomic hpos
[GOAL]
R✝ : Type u_1
inst✝⁵ : CommRing R✝
n✝ : ℕ
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
⊢ cyclotomic n K = minpoly K μ
[PROOFSTEP]
haveI := NeZero.of_noZeroSMulDivisors K R n
[GOAL]
R✝ : Type u_1
inst✝⁵ : CommRing R✝
n✝ : ℕ
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ cyclotomic n K = minpoly K μ
[PROOFSTEP]
refine' minpoly.eq_of_irreducible_of_monic h _ (cyclotomic.monic n K)
[GOAL]
R✝ : Type u_1
inst✝⁵ : CommRing R✝
n✝ : ℕ
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ ↑(aeval μ) (cyclotomic n K) = 0
[PROOFSTEP]
rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ cyclotomic n ℤ = minpoly ℤ μ
[PROOFSTEP]
refine'
  eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic (IsPrimitiveRoot.isIntegral h hpos)) (cyclotomic.monic n ℤ)
    (h.minpoly_dvd_cyclotomic hpos) _
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ natDegree (cyclotomic n ℤ) ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
simpa [natDegree_cyclotomic n ℤ] using totient_le_degree_minpoly h
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ cyclotomic n ℚ = minpoly ℚ μ
[PROOFSTEP]
rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos]
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ
[PROOFSTEP]
exact (minpoly.isIntegrallyClosed_eq_field_fractions' _ (IsPrimitiveRoot.isIntegral h hpos)).symm
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ Irreducible (cyclotomic n ℤ)
[PROOFSTEP]
rw [cyclotomic_eq_minpoly (isPrimitiveRoot_exp n hpos.ne') hpos]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ Irreducible (minpoly ℤ (exp (2 * ↑Real.pi * I / ↑n)))
[PROOFSTEP]
apply minpoly.irreducible
[GOAL]
case hx
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ IsIntegral ℤ (exp (2 * ↑Real.pi * I / ↑n))
[PROOFSTEP]
exact (isPrimitiveRoot_exp n hpos.ne').isIntegral hpos
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ Irreducible (cyclotomic n ℚ)
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))
[PROOFSTEP]
exact
  (IsPrimitive.irreducible_iff_irreducible_map_fraction_map (cyclotomic.isPrimitive n ℤ)).1
    (cyclotomic.irreducible hpos)
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n m : ℕ
h : n ≠ m
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hnzero)
[GOAL]
case inl
R : Type u_1
inst✝ : CommRing R
n m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)
[PROOFSTEP]
exact isCoprime_one_left
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n✝ n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
[PROOFSTEP]
rcases m.eq_zero_or_pos with (rfl | hmzero)
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)
[PROOFSTEP]
exact isCoprime_one_right
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommRing R
n✝ n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
[PROOFSTEP]
rw [Irreducible.coprime_iff_not_dvd <| cyclotomic.irreducible_rat <| hnzero]
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommRing R
n✝ n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ ¬cyclotomic n ℚ ∣ cyclotomic m ℚ
[PROOFSTEP]
exact fun hdiv =>
  h <|
    cyclotomic_injective <|
      eq_of_monic_of_associated (cyclotomic.monic n ℚ) (cyclotomic.monic m ℚ) <|
        Irreducible.associated_of_dvd (cyclotomic.irreducible_rat hnzero) (cyclotomic.irreducible_rat hmzero) hdiv


[GOAL]
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ IsWeaklyEisensteinAt (Polynomial.map φ f) (Ideal.map φ 𝓟)
[PROOFSTEP]
refine' (IsWeaklyEisensteinAt_iff _ _).2 fun hn => _
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < natDegree (Polynomial.map φ f)
⊢ coeff (Polynomial.map φ f) n✝ ∈ Ideal.map φ 𝓟
[PROOFSTEP]
rw [coeff_map]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < natDegree (Polynomial.map φ f)
⊢ ↑φ (coeff f n✝) ∈ Ideal.map φ 𝓟
[PROOFSTEP]
exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn (natDegree_map_le _ _)))
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
rw [aeval_def, Polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one, sum_insert not_mem_range_self, sum_range,
  (hmo.map (algebraMap R S)).coeff_natDegree, one_mul] at hx
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) +
      ∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i =
    0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
replace hx := eq_neg_of_add_eq_zero_left hx
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
have : ∀ n < f.natDegree, p ∣ f.coeff n := by
  intro n hn
  refine' mem_span_singleton.1 (by simpa using hf.mem hn)
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
⊢ ∀ (n : ℕ), n < natDegree f → p ∣ coeff f n
[PROOFSTEP]
intro n hn
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
n : ℕ
hn : n < natDegree f
⊢ p ∣ coeff f n
[PROOFSTEP]
refine' mem_span_singleton.1 (by simpa using hf.mem hn)
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
n : ℕ
hn : n < natDegree f
⊢ coeff f n ∈ span {p}
[PROOFSTEP]
simpa using hf.mem hn
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
this : ∀ (n : ℕ), n < natDegree f → p ∣ coeff f n
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
choose! φ hφ using this
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
conv_rhs at hx =>
  congr
  congr
  ·skip
  ext i
  rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)), RingHom.map_mul, mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
  congr
  congr
  ·skip
  ext i
  rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)), RingHom.map_mul, mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
  congr
  congr
  ·skip
  ext i
  rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)), RingHom.map_mul, mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| ∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
congr
[GOAL]
case a.s
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| univ
case a.f
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| fun i => coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
·skip
[GOAL]
case a.s
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| univ
[PROOFSTEP]
skip
[GOAL]
case a.s
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| univ
[PROOFSTEP]
skip
[GOAL]
case a.s
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| univ
[PROOFSTEP]
skip
[GOAL]
case a.f
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| fun i => coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
ext i
[GOAL]
case a.f.h
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
i : Fin (natDegree (Polynomial.map (algebraMap R S) f))
| coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)), RingHom.map_mul, mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)),
        ↑(algebraMap R S) p * (↑(algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)),
        ↑(algebraMap R S) p * (↑(algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
⊢ ∃ y,
    y ∈ adjoin R {x} ∧
      ↑(algebraMap R S) p * y =
        ↑(algebraMap R S) p *
          (-1 * ∑ x_1 : Fin (natDegree (Polynomial.map (algebraMap R S) f)), ↑(algebraMap R S) (φ ↑x_1) * x ^ ↑x_1)
[PROOFSTEP]
refine' ⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, _, rfl⟩
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)),
        ↑(algebraMap R S) p * (↑(algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
⊢ -1 * ∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), ↑(algebraMap R S) (φ ↑i) * x ^ ↑i ∈ adjoin R {x}
[PROOFSTEP]
exact
  Subalgebra.mul_mem _ (Subalgebra.neg_mem _ (Subalgebra.one_mem _))
    (Subalgebra.sum_mem _ fun i _ =>
      Subalgebra.mul_mem _ (Subalgebra.algebraMap_mem _ _)
        (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _))
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ i
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ i
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_add_of_le hi
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ i
[PROOFSTEP]
rw [hk, pow_add]
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
[PROOFSTEP]
obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_natDegree hx hmo hf
[GOAL]
case intro.intro.intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
[PROOFSTEP]
refine' ⟨y * x ^ k, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ y * x ^ k ∈ adjoin R {x}
[PROOFSTEP]
exact Subalgebra.mul_mem _ hy (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _)
[GOAL]
case intro.intro.intro.refine'_2
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ↑(algebraMap R S) p * (y * x ^ k) = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
[PROOFSTEP]
rw [← mul_assoc _ y, H]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
⊢ ∀ (i : ℕ), natDegree f ≤ i → x ^ i ∈ 𝓟
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
⊢ x ^ i ∈ 𝓟
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_add_of_le hi
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ i ∈ 𝓟
[PROOFSTEP]
rw [hk, pow_add]
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f * x ^ k ∈ 𝓟
[PROOFSTEP]
suffices x ^ f.natDegree ∈ 𝓟 by exact mul_mem_right (x ^ k) 𝓟 this
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
this : x ^ natDegree f ∈ 𝓟
⊢ x ^ natDegree f * x ^ k ∈ 𝓟
[PROOFSTEP]
exact mul_mem_right (x ^ k) 𝓟 this
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f ∈ 𝓟
[PROOFSTEP]
rw [IsRoot.def, eval_eq_sum_range, Finset.range_add_one, Finset.sum_insert Finset.not_mem_range_self, Finset.sum_range,
  hmo.coeff_natDegree, one_mul] at *
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : x ^ natDegree f + ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i = 0
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f ∈ 𝓟
[PROOFSTEP]
rw [eq_neg_of_add_eq_zero_left hroot, Ideal.neg_mem_iff]
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : x ^ natDegree f + ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i = 0
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i ∈ 𝓟
[PROOFSTEP]
refine' Submodule.sum_mem _ fun i _ => mul_mem_right _ _ (hf.mem (Fin.is_lt i))
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
suffices x ^ (f.map (algebraMap R S)).natDegree ∈ 𝓟.map (algebraMap R S)
  by
  intro i hi
  obtain ⟨k, hk⟩ := exists_add_of_le hi
  rw [hk, pow_add]
  refine' mul_mem_right _ _ this
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_add_of_le hi
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
rw [hk, pow_add]
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
refine' mul_mem_right _ _ this
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsRoot (Polynomial.map (algebraMap R S) f) x
hmo : Monic f
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
refine' pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
⊢ IsWeaklyEisensteinAt (scaleRoots p x) P
[PROOFSTEP]
refine' ⟨fun i => _⟩
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < natDegree (scaleRoots p x)
⊢ coeff (scaleRoots p x) n✝ ∈ P
[PROOFSTEP]
rw [coeff_scaleRoots]
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < natDegree (scaleRoots p x)
⊢ coeff p n✝ * x ^ (natDegree p - n✝) ∈ P
[PROOFSTEP]
rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i✝ : n✝ < natDegree p
i : 0 < natDegree p - n✝
⊢ coeff p n✝ * x ^ (natDegree p - n✝) ∈ P
[PROOFSTEP]
exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ x ∣ y ^ natDegree p
[PROOFSTEP]
rw [← natDegree_scaleRoots p x, ← Ideal.mem_span_singleton]
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ y ^ natDegree (scaleRoots p x) ∈ span {x}
[PROOFSTEP]
refine'
  (scaleRoots.isWeaklyEisensteinAt _ (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
    _ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ IsRoot (scaleRoots p x) y
[PROOFSTEP]
rw [injective_iff_map_eq_zero'] at hf
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), ↑f a = 0 ↔ a = 0
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ IsRoot (scaleRoots p x) y
[PROOFSTEP]
have : eval₂ _ _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), ↑f a = 0 ↔ a = 0
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
this : eval₂ f (↑f x * z) (scaleRoots p x) = 0
⊢ IsRoot (scaleRoots p x) y
[PROOFSTEP]
rwa [hz, Polynomial.eval₂_at_apply, hf] at this
[GOAL]
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
⊢ coeff f n ∈ 𝓟
[PROOFSTEP]
cases' ne_iff_lt_or_gt.1 hn with h₁ h₂
[GOAL]
case inl
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₁ : n < natDegree f
⊢ coeff f n ∈ 𝓟
[PROOFSTEP]
exact hf.mem h₁
[GOAL]
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₂ : n > natDegree f
⊢ coeff f n ∈ 𝓟
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt h₂]
[GOAL]
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₂ : n > natDegree f
⊢ 0 ∈ 𝓟
[PROOFSTEP]
exact Ideal.zero_mem _