R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (n + 1)) R = ∑ i in range p, (X ^ p ^ n) ^ i
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
⊢ cyclotomic (p ^ (n + 1)) R = ∑ i in range p, (X ^ p ^ n) ^ i
have : ∀ m, (cyclotomic (p ^ (m + 1)) R = ∑ i in Finset.range p, (X ^ p ^ m) ^ i) ↔
    ((∑ i in Finset.range p, (X ^ p ^ m) ^ i) *
      ∏ x : ℕ in Finset.range (m + 1), cyclotomic (p ^ x) R) = X ^ p ^ (m + 1) - 1 := by
  intro m
  have := eq_cyclotomic_iff (R := R) (P := ∑ i in range p, (X ^ p ^ m) ^ i)
    (pow_pos hp.pos (m + 1))
  rw [eq_comm] at this
  rw [this, Nat.prod_properDivisors_prime_pow hp]
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (Nat.zero + 1)) R = ∑ i in range p, (X ^ p ^ Nat.zero) ^ i

case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ cyclotomic (p ^ (Nat.succ n_n + 1)) R = ∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (n + 1)) R = ∑ i in range p, (X ^ p ^ n) ^ i
induction' n with n_n n_ih
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) * ∏ i in Nat.properDivisors (p ^ (Nat.succ n_n + 1)), cyclotomic i R =
    X ^ p ^ (Nat.succ n_n + 1) - 1
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ cyclotomic (p ^ (Nat.succ n_n + 1)) R = ∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i
rw [((eq_cyclotomic_iff (pow_pos hp.pos (n_n.succ + 1)) _).mpr _).symm]
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) *
      ((∏ x in range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i in range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (Nat.succ n_n + 1) - 1
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) * ∏ i in Nat.properDivisors (p ^ (Nat.succ n_n + 1)), cyclotomic i R =
    X ^ p ^ (Nat.succ n_n + 1) - 1
rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i in range p, (X ^ p ^ n_n) ^ i) * ∏ x in range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) *
      ((∏ x in range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i in range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (Nat.succ n_n + 1) - 1
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) *
      ((∏ x in range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i in range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (Nat.succ n_n + 1) - 1
rw [this] at n_ih
no goals
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i in range p, (X ^ p ^ n_n) ^ i) * ∏ x in range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) *
      ((∏ x in range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i in range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (Nat.succ n_n + 1) - 1
rw [mul_comm _ (∑ i in _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul, pow_add, pow_one]
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
⊢ ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
intro m
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  ∑ i in range p, (X ^ p ^ m) ^ i = cyclotomic (p ^ (m + 1)) R ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ i in Nat.properDivisors (p ^ (m + 1)), cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
have := eq_cyclotomic_iff (R := R) (P := ∑ i in range p, (X ^ p ^ m) ^ i)
  (pow_pos hp.pos (m + 1))
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ i in Nat.properDivisors (p ^ (m + 1)), cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  ∑ i in range p, (X ^ p ^ m) ^ i = cyclotomic (p ^ (m + 1)) R ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ i in Nat.properDivisors (p ^ (m + 1)), cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
rw [eq_comm] at this
no goals
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ i in Nat.properDivisors (p ^ (m + 1)), cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
rw [this, Nat.prod_properDivisors_prime_pow hp]
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this✝ :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
this : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (Nat.zero + 1)) R = ∑ i in range p, (X ^ p ^ Nat.zero) ^ i
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (Nat.zero + 1)) R = ∑ i in range p, (X ^ p ^ Nat.zero) ^ i
haveI := Fact.mk hp
no goals
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this✝ :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
this : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (Nat.zero + 1)) R = ∑ i in range p, (X ^ p ^ Nat.zero) ^ i
simp [cyclotomic_prime]