Theorem: zeta_sub_one_dvd_Int_iff (FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
n : ℤ
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n
Tactic:
clear hp
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ K
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n
Tactic:
by_cases hp : p = 2
State after:
case pos
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : p = 2
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n

case neg
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : ¬p = 2
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n

State before:
case neg
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : ¬p = 2
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n
Tactic:
rw [← norm_Int_zeta_sub_one hζ hp, norm_dvd_iff]
State after:
case neg.hx
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : ¬p = 2
⊢ Prime ((Algebra.norm ℤ) (↑hζ.unit' - 1))

State before:
case neg.hx
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : ¬p = 2
⊢ Prime ((Algebra.norm ℤ) (↑hζ.unit' - 1))
Tactic:
rw [norm_Int_zeta_sub_one hζ hp, ← Nat.prime_iff_prime_int]
State after:
case neg.hx
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : ¬p = 2
⊢ (↑p).Prime

State before:
case neg.hx
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : ¬p = 2
⊢ (↑p).Prime
Tactic:
exact hpri.out
State after:
no goals

State before:
case pos
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : p = 2
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑p ∣ n
Tactic:
rw [← neg_dvd (a := (p : ℤ))]
State after:
case pos
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : p = 2
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ -↑↑p ∣ n

State before:
case pos
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : p = 2
⊢ ↑hζ.unit' - 1 ∣ ↑n ↔ -↑↑p ∣ n
Tactic:
rw [← norm_Int_zeta_sub_one' hζ hp, norm_dvd_iff]
State after:
case pos.hx
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : p = 2
⊢ Prime ((Algebra.norm ℤ) (↑hζ.unit' - 1))

State before:
case pos.hx
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : p = 2
⊢ Prime ((Algebra.norm ℤ) (↑hζ.unit' - 1))
Tactic:
rw [norm_Int_zeta_sub_one' hζ hp, prime_neg_iff, ← Nat.prime_iff_prime_int]
State after:
case pos.hx
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : p = 2
⊢ (↑p).Prime

State before:
case pos.hx
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
hp : p = 2
⊢ (↑p).Prime
Tactic:
exact hpri.out
State after:
no goals