internlm/Lean-Github huggingface dataset:
Theorem: exists_zeta_sub_one_dvd_sub_Int
Proof state before:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.subOneIntegralPowerBasis'.gen
Tactic:
rw [hζ.subOneIntegralPowerBasis'_gen]
Proof state after:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.toInteger - 1
Theorem: exists_zeta_sub_one_dvd_sub_Int
Proof state before:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.toInteger - 1
Tactic:
rw [Subtype.ext_iff, AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one]
Proof state after:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ζ - 1 = ↑(hζ.toInteger - 1)
Theorem: exists_zeta_sub_one_dvd_sub_Int
Proof state before:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ζ - 1 = ↑(hζ.toInteger - 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: exists_dvd_pow_sub_Int_pow
Proof 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
a : 𝓞 K
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root ℚ (B := K) (Set.mem_singleton p)
Proof state after:
case intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Theorem: exists_dvd_pow_sub_Int_pow
Proof state before:
case intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
obtain ⟨b, k, e⟩ := exists_zeta_sub_one_dvd_sub_Int hζ a
Proof state after:
case intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Theorem: exists_dvd_pow_sub_Int_pow
Proof state before:
case intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
obtain ⟨r, hr⟩ := exists_add_pow_prime_eq hpri.out a (-b)
Proof state after:
case intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Theorem: exists_dvd_pow_sub_Int_pow
Proof state before:
case intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
obtain ⟨u, hu⟩ := (associated_zeta_sub_one_pow_prime hζ).symm
Proof state after:
case intro.intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Theorem: exists_dvd_pow_sub_Int_pow
Proof state before:
case intro.intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
rw [(Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)).neg_pow, ← sub_eq_add_neg, e,
  mul_pow, ← sub_eq_add_neg] at hr
Proof state after:
case intro.intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ ↑p * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Theorem: exists_dvd_pow_sub_Int_pow
Proof state before:
case intro.intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ ↑p * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
nth_rw 1 [← Nat.sub_add_cancel (n := p) (m := 1) hpri.out.one_lt.le] at hr
Proof state after:
case intro.intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ (↑p - 1 + 1) * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Theorem: exists_dvd_pow_sub_Int_pow
Proof state before:
case intro.intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ (↑p - 1 + 1) * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
rw [pow_succ, ← hu, mul_assoc, mul_assoc] at hr
Proof state after:
case intro.intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Theorem: exists_dvd_pow_sub_Int_pow
Proof state before:
case intro.intro.intro.intro.intro
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
use b, ↑u * ((hζ.unit' - 1 : 𝓞 K) * k ^ (p : ℕ)) - r
Proof state after:
case h
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ a ^ ↑p - ↑b ^ ↑p = ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p) - r)
Theorem: exists_dvd_pow_sub_Int_pow
Proof state before:
case h
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
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ a ^ ↑p - ↑b ^ ↑p = ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p) - r)
Tactic:
rw [mul_sub, hr, add_sub_cancel_right]
Proof state after:
no goals
Theorem: norm_dvd_iff
Proof 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
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y
Tactic:
rw [← Ideal.mem_span_singleton (y := x), ← eq_intCast (algebraMap ℤ R), ← Ideal.mem_comap,
  ← Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Ideal.absNorm_span_singleton,
  Int.natAbs_dvd]
Proof 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
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Ideal.absNorm (Ideal.span {x})).Prime
Theorem: norm_dvd_iff
Proof 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
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Ideal.absNorm (Ideal.span {x})).Prime
Tactic:
rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]
Proof state after:
no goals
Theorem: prime_units_mul
Proof 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
α : Type u_2
inst✝ : CommMonoidWithZero α
a : αˣ
b : α
⊢ Prime (↑a * b) ↔ Prime b
Tactic:
simp [Prime]
Proof state after:
no goals
Theorem: prime_mul_units
Proof 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
α : Type u_2
inst✝ : CommMonoidWithZero α
a : αˣ
b : α
⊢ Prime (b * ↑a) ↔ Prime b
Tactic:
simp [Prime]
Proof state after:
no goals
Theorem: prime_neg_iff
Proof 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
α✝ : Type ?u.198894
inst✝¹ : CommMonoidWithZero α✝
α : Type u_2
inst✝ : CommRing α
a : α
⊢ Prime (-a) ↔ Prime a
Tactic:
rw [← prime_isUnit_mul isUnit_one.neg, neg_mul, one_mul, neg_neg]
Proof state after:
no goals
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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
Proof 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
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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
Proof 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
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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
Proof 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
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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]
Proof 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))
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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]
Proof 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
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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
Proof state after:
no goals
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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 : ℤ))]
Proof 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
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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]
Proof 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))
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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]
Proof 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
Theorem: zeta_sub_one_dvd_Int_iff
Proof 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
Proof state after:
no goals
Theorem: IsPrimitiveRoot.sub_one_dvd_sub
Proof 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
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
⊢ ζ - 1 ∣ η₁ - η₂
Tactic:
by_cases h : η₁ = η₂
Proof 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✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : η₁ = η₂
⊢ ζ - 1 ∣ η₁ - η₂

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✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : ¬η₁ = η₂
⊢ ζ - 1 ∣ η₁ - η₂
Theorem: IsPrimitiveRoot.sub_one_dvd_sub
Proof 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✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : η₁ = η₂
⊢ ζ - 1 ∣ η₁ - η₂
Tactic:
rw [h, sub_self]
Proof 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✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : η₁ = η₂
⊢ ζ - 1 ∣ 0
Theorem: IsPrimitiveRoot.sub_one_dvd_sub
Proof 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✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : η₁ = η₂
⊢ ζ - 1 ∣ 0
Tactic:
exact dvd_zero _
Proof state after:
no goals
Theorem: IsPrimitiveRoot.sub_one_dvd_sub
Proof 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✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : ¬η₁ = η₂
⊢ ζ - 1 ∣ η₁ - η₂
Tactic:
exact (hζ.associated_sub_one hp hη₁ hη₂ h).dvd
Proof state after:
no goals
Theorem: quotient_zero_sub_one_comp_aut
Proof 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
σ : 𝓞 K →+* 𝓞 K
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Tactic:
have : Fact (Nat.Prime p) := hpri
Proof 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
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this : Fact (↑p).Prime
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Theorem: quotient_zero_sub_one_comp_aut
Proof 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
σ : 𝓞 K →+* 𝓞 K
this : Fact (↑p).Prime
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ K
Proof 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
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Theorem: quotient_zero_sub_one_comp_aut
Proof 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
σ : 𝓞 K →+* 𝓞 K
this✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Tactic:
letI : AddGroup (𝓞 K ⧸ Ideal.span (singleton (hζ.unit' - 1: 𝓞 K))) := inferInstance
Proof 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
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})