[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
[PROOFSTEP]
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
[GOAL]
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝ : CommRing R
hdiv : ¬p ∣ 0
⊢ ↑(expand R p) (cyclotomic 0 R) = cyclotomic (0 * p) R * cyclotomic 0 R
[PROOFSTEP]
simp
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
[PROOFSTEP]
haveI := NeZero.of_pos hnpos
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
[PROOFSTEP]
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ by
  rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic]
[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this✝ : NeZero n
this : ↑(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
[PROOFSTEP]
rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic]
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ ↑(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
[PROOFSTEP]
refine'
  eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (cyclotomic.monic _ _))
    ((cyclotomic.monic n ℤ).expand hp.pos) _ _
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
refine'
  (IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast _ _
        (IsPrimitive.mul (cyclotomic.isPrimitive (n * p) ℤ) (cyclotomic.isPrimitive n ℤ))
        ((cyclotomic.monic n ℤ).expand hp.pos).isPrimitive).2
    _
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ map (Int.castRingHom ℚ) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) ∣
    map (Int.castRingHom ℚ) (↑(expand ℤ p) (cyclotomic n ℤ))
[PROOFSTEP]
rw [Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, map_cyclotomic_int]
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
refine' IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => _) _ _
[GOAL]
case inr.refine'_1.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n
⊢ False
[PROOFSTEP]
replace h : n * p = n * 1 := by simp [h]
[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n
⊢ n * p = n * 1
[PROOFSTEP]
simp [h]
[GOAL]
case inr.refine'_1.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n * 1
⊢ False
[PROOFSTEP]
exact Nat.Prime.ne_one hp (mul_left_cancel₀ hnpos.ne' h)
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
have hpos : 0 < n * p := mul_pos hnpos hp.pos
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
⊢ cyclotomic (n * p) ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ cyclotomic (n * p) ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
rw [cyclotomic_eq_minpoly_rat hprim hpos]
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
refine' @minpoly.dvd ℚ ℂ _ _ algebraRat _ _ _
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ ↑(aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)))) (↑(expand ℚ p) (cyclotomic n ℚ)) = 0
[PROOFSTEP]
rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def, @isRoot_cyclotomic_iff]
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)) ^ p) n
[PROOFSTEP]
convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
[GOAL]
case h.e'_4
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ n = n * p / p
[PROOFSTEP]
rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)]
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic n ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ cyclotomic n ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
rw [cyclotomic_eq_minpoly_rat hprim hnpos]
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) ∣
    ↑(expand ℚ p) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))
[PROOFSTEP]
refine' @minpoly.dvd ℚ ℂ _ _ algebraRat _ _ _
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ ↑(aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))
      (↑(expand ℚ p) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))) =
    0
[PROOFSTEP]
rw [aeval_def, ← eval_map, map_expand, expand_eval, ← IsRoot.def, ← cyclotomic_eq_minpoly_rat hprim hnpos,
  map_cyclotomic, @isRoot_cyclotomic_iff]
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) ^ p) n
[PROOFSTEP]
exact IsPrimitiveRoot.pow_of_prime hprim hp hdiv
[GOAL]
case inr.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ natDegree (↑(expand ℤ p) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ * cyclotomic n ℤ)
[PROOFSTEP]
rw [natDegree_expand, natDegree_cyclotomic, natDegree_mul (cyclotomic_ne_zero _ ℤ) (cyclotomic_ne_zero _ ℤ),
  natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n, Nat.totient_mul ((Nat.Prime.coprime_iff_not_dvd hp).2 hdiv),
  Nat.totient_prime hp, mul_comm (p - 1), ← Nat.mul_succ, Nat.sub_one, Nat.succ_pred_eq_of_pos hp.pos]
[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hzero)
[GOAL]
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝ : CommRing R
hdiv : p ∣ 0
⊢ ↑(expand R p) (cyclotomic 0 R) = cyclotomic (0 * p) R
[PROOFSTEP]
simp
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
[PROOFSTEP]
haveI := NeZero.of_pos hzero
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
[PROOFSTEP]
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ by
  rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int, map_cyclotomic]
[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this✝ : NeZero n
this : ↑(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
[PROOFSTEP]
rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int, map_cyclotomic]
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ ↑(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
[PROOFSTEP]
refine' eq_of_monic_of_dvd_of_natDegree_le (cyclotomic.monic _ _) ((cyclotomic.monic n ℤ).expand hp.pos) _ _
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℤ ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
have hpos := Nat.mul_pos hzero hp.pos
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
⊢ cyclotomic (n * p) ℤ ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne.symm
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ cyclotomic (n * p) ℤ ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
rw [cyclotomic_eq_minpoly hprim hpos]
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ minpoly ℤ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
refine' minpoly.isIntegrallyClosed_dvd (hprim.isIntegral hpos) _
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ ↑(aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)))) (↑(expand ℤ p) (cyclotomic n ℤ)) = 0
[PROOFSTEP]
rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def, @isRoot_cyclotomic_iff]
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)) ^ p) n
[PROOFSTEP]
convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
[GOAL]
case h.e'_4
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ n = n * p / p
[PROOFSTEP]
rw [Nat.mul_div_cancel _ hp.pos]
[GOAL]
case inr.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ natDegree (↑(expand ℤ p) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
[PROOFSTEP]
rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n, Nat.totient_mul_of_prime_of_dvd hp hdiv,
  mul_comm]
[GOAL]
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
rcases m.eq_zero_or_pos with (rfl | hm)
[GOAL]
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : Irreducible (cyclotomic (p ^ n) R)
hmn : 0 ≤ n
⊢ Irreducible (cyclotomic (p ^ 0) R)
[PROOFSTEP]
simpa using irreducible_X_sub_C (1 : R)
[GOAL]
case inr
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
hm : m > 0
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
[GOAL]
case inr.intro
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn : m ≤ m + k
h : Irreducible (cyclotomic (p ^ (m + k)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
induction' k with k hk
[GOAL]
case inr.intro.zero
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn✝ : m ≤ m + k
h✝ : Irreducible (cyclotomic (p ^ (m + k)) R)
hmn : m ≤ m + Nat.zero
h : Irreducible (cyclotomic (p ^ (m + Nat.zero)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
simpa using h
[GOAL]
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k✝ : ℕ
hmn✝ : m ≤ m + k✝
h✝ : Irreducible (cyclotomic (p ^ (m + k✝)) R)
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + Nat.succ k
h : Irreducible (cyclotomic (p ^ (m + Nat.succ k)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'
[GOAL]
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k✝ : ℕ
hmn✝ : m ≤ m + k✝
h✝ : Irreducible (cyclotomic (p ^ (m + k✝)) R)
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + Nat.succ k
h : Irreducible (cyclotomic (p ^ (m + Nat.succ k)) R)
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
rw [Nat.add_succ, pow_succ', ← cyclotomic_expand_eq_cyclotomic hp <| dvd_pow_self p this] at h 
[GOAL]
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k✝ : ℕ
hmn✝ : m ≤ m + k✝
h✝ : Irreducible (cyclotomic (p ^ (m + k✝)) R)
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + Nat.succ k
h : Irreducible (↑(expand R p) (cyclotomic (p ^ (m + k)) R))
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
exact hk (by linarith) (of_irreducible_expand hp.ne_zero h)
[GOAL]
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k✝ : ℕ
hmn✝ : m ≤ m + k✝
h✝ : Irreducible (cyclotomic (p ^ (m + k✝)) R)
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + Nat.succ k
h : Irreducible (↑(expand R p) (cyclotomic (p ^ (m + k)) R))
this : m + k ≠ 0
⊢ m ≤ m + k
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)
[PROOFSTEP]
letI : Algebra (ZMod p) R := ZMod.algebra _ _
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)
[PROOFSTEP]
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1) by
  rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)
[PROOFSTEP]
rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
[PROOFSTEP]
apply mul_right_injective₀ (cyclotomic_ne_zero n <| ZMod p)
[GOAL]
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (fun x x_1 => x * x_1) (cyclotomic n (ZMod p)) (cyclotomic (n * p) (ZMod p)) =
    (fun x x_1 => x * x_1) (cyclotomic n (ZMod p)) (cyclotomic n (ZMod p) ^ (p - 1))
[PROOFSTEP]
dsimp
[GOAL]
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) * cyclotomic n (ZMod p) ^ (p - 1)
[PROOFSTEP]
rw [← pow_succ, tsub_add_cancel_of_le hp.out.one_lt.le, mul_comm, ← ZMod.expand_card]
[GOAL]
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) = ↑(expand (ZMod p) p) (cyclotomic n (ZMod p))
[PROOFSTEP]
conv_rhs => rw [← map_cyclotomic_int]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(expand (ZMod p) p) (cyclotomic n (ZMod p))
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(expand (ZMod p) p) (cyclotomic n (ZMod p))
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(expand (ZMod p) p) (cyclotomic n (ZMod p))
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) =
    ↑(expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
[PROOFSTEP]
rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul, map_cyclotomic, map_cyclotomic]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p
[PROOFSTEP]
letI : Algebra (ZMod p) R := ZMod.algebra _ _
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p
[PROOFSTEP]
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p by
  rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p
[PROOFSTEP]
rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p
[PROOFSTEP]
rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand, cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic,
  mul_comm]
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
x✝ : 0 < 1
⊢ cyclotomic (p ^ 1 * m) R = cyclotomic m R ^ (p ^ 1 - p ^ (1 - 1))
[PROOFSTEP]
rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
⊢ cyclotomic (p ^ (a + 2) * m) R = cyclotomic m R ^ (p ^ (a + 2) - p ^ (a + 2 - 1))
[PROOFSTEP]
have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ]⟩
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
⊢ p ^ Nat.succ a * m = p * (p ^ a * m)
[PROOFSTEP]
rw [← mul_assoc, pow_succ]
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ cyclotomic (p ^ (a + 2) * m) R = cyclotomic m R ^ (p ^ (a + 2) - p ^ (a + 2 - 1))
[PROOFSTEP]
rw [pow_succ, mul_assoc, mul_comm, cyclotomic_mul_prime_dvd_eq_pow R hdiv, cyclotomic_mul_prime_pow_eq _ _ a.succ_pos, ←
  pow_mul]
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ cyclotomic m R ^ ((p ^ Nat.succ a - p ^ (Nat.succ a - 1)) * p) = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 2 - 1))
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ ¬p ∣ m
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ (p ^ Nat.succ a - p ^ (Nat.succ a - 1)) * p = p * p ^ (a + 1) - p ^ (a + 2 - 1)
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ ¬p ∣ m
[PROOFSTEP]
simp only [tsub_zero, Nat.succ_sub_succ_eq_sub]
[GOAL]
case e_a
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ (p ^ Nat.succ a - p ^ a) * p = p * p ^ (a + 1) - p ^ (a + 1)
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ ¬p ∣ m
[PROOFSTEP]
rwa [Nat.mul_sub_right_distrib, mul_comm, pow_succ']
[GOAL]
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
[PROOFSTEP]
rcases k.eq_zero_or_pos with (rfl | hk)
[GOAL]
case inl
m p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ IsRoot (cyclotomic (p ^ 0 * m) R) μ ↔ IsPrimitiveRoot μ m
[PROOFSTEP]
rw [pow_zero, one_mul, isRoot_cyclotomic_iff]
[GOAL]
case inr
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case inr.refine'_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsRoot (cyclotomic (p ^ k * m) R) μ
⊢ IsPrimitiveRoot μ m
[PROOFSTEP]
rw [IsRoot.def, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow] at h 
[GOAL]
case inr.refine'_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)) = 0
⊢ IsPrimitiveRoot μ m
[PROOFSTEP]
replace h := pow_eq_zero h
[GOAL]
case inr.refine'_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ IsPrimitiveRoot μ m
[PROOFSTEP]
rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h 
[GOAL]
case inr.refine'_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsPrimitiveRoot μ m
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ
[PROOFSTEP]
rw [← isRoot_cyclotomic_iff, IsRoot.def] at h 
[GOAL]
case inr.refine'_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ
[PROOFSTEP]
rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow, h, zero_pow]
[GOAL]
case inr.refine'_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ 0 < p ^ k - p ^ (k - 1)
[PROOFSTEP]
simp only [tsub_pos_iff_lt]
[GOAL]
case inr.refine'_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ p ^ (k - 1) < p ^ k
[PROOFSTEP]
apply pow_strictMono_right hp.out.one_lt (Nat.pred_lt hk.ne')
