case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ orderOf (ZMod.unitOfCoprime a (_ : Nat.coprime a p)) ∣ n
apply orderOf_dvd_of_pow_eq_one
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1

case hpow
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1
suffices hpow : eval (Nat.castRingHom (ZMod p) a) (X ^ n - 1 : (ZMod p)[X]) = 0
case hpow
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval (↑(Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
case hpow
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
rw [IsRoot.def] at hroot
no goals
case hpow
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval (↑(Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne',
  Finset.prod_cons, eval_mul, hroot, MulZeroClass.zero_mul]
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1
simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ↑(ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n) = 1
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1
apply Units.val_eq_one.1
no goals
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ↑(ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n) = 1
simp only [sub_eq_zero.mp hpow, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val]