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

State before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Tactic:
letI p' : ℕ+ := ⟨p, hpri.out.pos⟩
State after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n

State before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Tactic:
letI : Fact (PNat.Prime p') := hpri
State after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n

State before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Tactic:
letI H := IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
State after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n

State before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Tactic:
rw [← map_dvd_iff (equiv p), map_sub, map_one, equiv_zeta, map_intCast,
  ← neg_dvd, neg_sub]
State after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ ⋯.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n

State before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ ⋯.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n
Tactic:
exact zeta_sub_one_dvd_Int_iff H
State after:
no goals