K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = cyclotomic' n K
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = ∏ μ in primitiveRoots n K, (X - ↑C μ)
rw [← cyclotomic']
case h
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
⊢ cyclotomic k K = cyclotomic' k K
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = cyclotomic' n K
induction' n using Nat.strong_induction_on with k hk generalizing ζ
case h.inl
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hzero : k = 0
⊢ cyclotomic k K = cyclotomic' k K

case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic k K = cyclotomic' k K
case h
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
⊢ cyclotomic k K = cyclotomic' k K
obtain hzero | hpos := k.eq_zero_or_pos
case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
h : ∀ (i : ℕ), i ∈ Nat.properDivisors k → cyclotomic i K = cyclotomic' i K
⊢ cyclotomic k K = cyclotomic' k K
case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic k K = cyclotomic' k K
have h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K := by
  intro i hi
  obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hi).1
  rw [mul_comm] at hd
  exact hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd)
no goals
case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
h : ∀ (i : ℕ), i ∈ Nat.properDivisors k → cyclotomic i K = cyclotomic' i K
⊢ cyclotomic k K = cyclotomic' k K
rw [@cyclotomic_eq_X_pow_sub_one_div _ _ _ hpos, cyclotomic'_eq_X_pow_sub_one_div hpos hz,
  Finset.prod_congr (refl k.properDivisors) h]
no goals
case h.inl
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hzero : k = 0
⊢ cyclotomic k K = cyclotomic' k K
simp only [hzero, cyclotomic'_zero, cyclotomic_zero]
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
⊢ cyclotomic i K = cyclotomic' i K
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors k → cyclotomic i K = cyclotomic' i K
intro i hi
case intro
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
d : ℕ
hd : k = i * d
⊢ cyclotomic i K = cyclotomic' i K
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
⊢ cyclotomic i K = cyclotomic' i K
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hi).1
case intro
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
d : ℕ
hd : k = d * i
⊢ cyclotomic i K = cyclotomic' i K
case intro
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
d : ℕ
hd : k = i * d
⊢ cyclotomic i K = cyclotomic' i K
rw [mul_comm] at hd
no goals
case intro
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
d : ℕ
hd : k = d * i
⊢ cyclotomic i K = cyclotomic' i K
exact hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd)