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

State before:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (1 - zeta p)
Tactic:
rw [← prime_units_mul (a := -1), Units.val_neg, Units.val_one, neg_mul, one_mul, neg_sub]
State after:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (zeta p - 1)

State before:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (zeta p - 1)
Tactic:
apply (equiv p).toMulEquiv.prime_iff.mpr
State after:
p : ℕ
hpri : Fact p.Prime
⊢ Prime ((equiv p).toMulEquiv (zeta p - 1))

State before:
p : ℕ
hpri : Fact p.Prime
⊢ Prime ((equiv p).toMulEquiv (zeta p - 1))
Tactic:
simp only [RingEquiv.toMulEquiv_eq_coe, RingEquiv.coe_toMulEquiv,
  (equiv p).map_sub, (equiv p).map_one, equiv_zeta]
State after:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (⋯.toInteger - 1)

State before:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (⋯.toInteger - 1)
Tactic:
letI p' : ℕ+ := ⟨p, hpri.out.pos⟩
State after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ Prime (⋯.toInteger - 1)

State before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ Prime (⋯.toInteger - 1)
Tactic:
letI : Fact (Nat.Prime p') := hpri
State after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ Prime (⋯.toInteger - 1)

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

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