case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic 0 R) =
    ∏ i in Nat.divisorsAntidiagonal 0, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst

case inr
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i in Nat.divisorsAntidiagonal n, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i in Nat.divisorsAntidiagonal n, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
rcases n.eq_zero_or_pos with (rfl | hpos)
case inr
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i in Nat.divisorsAntidiagonal n, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
case inr
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i in Nat.divisorsAntidiagonal n, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
have h : ∀ n : ℕ, 0 < n → (∏ i in Nat.divisors n, algebraMap _ (RatFunc R) (cyclotomic i R)) =
    algebraMap _ _ (X ^ n - 1 : R[X]) := by
  intro n hn
  rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬cyclotomic n R = 0

n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬X ^ n - 1 = 0
case inr
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i in Nat.divisorsAntidiagonal n, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
rw [(prod_eq_iff_prod_pow_moebius_eq_of_nonzero (fun n hn => _) fun n hn => _).1 h n hpos] <;>
  simp_rw [Ne.def, IsFractionRing.to_map_eq_zero_iff]
no goals
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic 0 R) =
    ∏ i in Nat.divisorsAntidiagonal 0, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
simp
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
n : ℕ
hn : 0 < n
⊢ ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) = ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
⊢ ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
intro n hn
no goals
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
n : ℕ
hn : 0 < n
⊢ ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) = ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
no goals
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬cyclotomic n R = 0
simp [cyclotomic_ne_zero]
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
n : ℕ
hn : 0 < n
⊢ ¬X ^ n - 1 = 0
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬X ^ n - 1 = 0
intro n hn
case hp
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
n : ℕ
hn : 0 < n
⊢ Monic (X ^ n - 1)
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
n : ℕ
hn : 0 < n
⊢ ¬X ^ n - 1 = 0
apply Monic.ne_zero
no goals
case hp
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
n : ℕ
hn : 0 < n
⊢ Monic (X ^ n - 1)
apply monic_X_pow_sub_C _ (ne_of_gt hn)