Theorem: CyclotomicIntegers.isCoprime_one_sub_zeta (FltRegular/NumberTheory/CyclotomicRing.lean)

State before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
hn : ¬↑p ∣ n
⊢ IsCoprime (1 - zeta p) ↑n
Tactic:
apply (((Nat.prime_iff_prime_int.mp hpri.out).coprime_iff_not_dvd.mpr hn).map
  (algebraMap ℤ <| CyclotomicIntegers p)).of_isCoprime_of_dvd_left
State after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
hn : ¬↑p ∣ n
⊢ 1 - zeta p ∣ (algebraMap ℤ (CyclotomicIntegers p)) ↑p

State before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
hn : ¬↑p ∣ n
⊢ 1 - zeta p ∣ (algebraMap ℤ (CyclotomicIntegers p)) ↑p
Tactic:
exact one_sub_zeta_dvd p
State after:
no goals