case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ Nat.coprime p a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ Nat.coprime a p
apply Nat.coprime.symm
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ ¬p ∣ a
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ Nat.coprime p a
rw [hprime.1.coprime_iff_not_dvd]
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
h : p ∣ a
⊢ False
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ ¬p ∣ a
intro h
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
h : ↑a = 0
⊢ False
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
h : p ∣ a
⊢ False
replace h := (ZMod.nat_cast_zmod_eq_zero_iff_dvd a p).2 h
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
⊢ False
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
h : ↑a = 0
⊢ False
rw [IsRoot.def, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot
case pos
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
hone : n = 1
⊢ False

case neg
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
hone : ¬n = 1
⊢ False
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
⊢ False
by_cases hone : n = 1
case neg
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : 1 = 0
h : ↑a = 0
hone : ¬n = 1
⊢ False
case neg
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
hone : ¬n = 1
⊢ False
rw [cyclotomic_coeff_zero (ZMod p) (Nat.succ_le_of_lt
  (lt_of_le_of_ne (Nat.succ_le_of_lt hpos) (Ne.symm hone)))] at hroot
no goals
case neg
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : 1 = 0
h : ↑a = 0
hone : ¬n = 1
⊢ False
exact one_ne_zero hroot
no goals
case pos
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
hone : n = 1
⊢ False
simp only [hone, cyclotomic_one, zero_sub, coeff_one_zero, coeff_X_zero, neg_eq_zero,
  one_ne_zero, coeff_sub] at hroot