internlm/Lean-Github huggingface dataset:
Theorem: surjective_of_isCyclotomicExtension_two
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | ∃ n ∈ {2}, b ^ ↑n = 1}
⊢ ∃ a, (algebraMap R S) a = x
Tactic:
simp only [Set.mem_singleton_iff, exists_eq_left, sq_eq_one_iff, PNat.coe_two] at this
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ ∃ a, (algebraMap R S) a = x
Theorem: surjective_of_isCyclotomicExtension_two
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
H : Algebra.adjoin R {b | b = 1 ∨ b = -1} ≤ ⊥
⊢ ∃ a, (algebraMap R S) a = x
Tactic:
exact H this
Proof state after:
no goals
Theorem: surjective_of_isCyclotomicExtension_two
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ Algebra.adjoin R {b | b = 1 ∨ b = -1} ≤ ⊥
Tactic:
rw [Algebra.adjoin_le_iff]
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ {b | b = 1 ∨ b = -1} ⊆ ↑⊥
Theorem: surjective_of_isCyclotomicExtension_two
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ {b | b = 1 ∨ b = -1} ⊆ ↑⊥
Tactic:
rintro _ (rfl|rfl)
Proof state after:
case inl
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ 1 ∈ ↑⊥

case inr
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ -1 ∈ ↑⊥
Theorem: surjective_of_isCyclotomicExtension_two
Proof state before:
case inl
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ 1 ∈ ↑⊥
Tactic:
exact one_mem _
Proof state after:
no goals
Theorem: surjective_of_isCyclotomicExtension_two
Proof state before:
case inr
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
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ -1 ∈ ↑⊥
Tactic:
exact neg_mem (one_mem _)
Proof state after:
no goals
Theorem: IsPrimitiveRoot.sub_one_norm_two'
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) (ζ - 1) = -2
Tactic:
rw [hζ.eq_neg_one_of_two_right]
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) (-1 - 1) = -2
Theorem: IsPrimitiveRoot.sub_one_norm_two'
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) (-1 - 1) = -2
Tactic:
suffices Algebra.norm K (algebraMap K L (-2)) = -2 by
  simpa only [sub_eq_add_neg, ← one_add_one_eq_two,
    neg_add_rev, map_add, map_neg, map_one] using this
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) ((algebraMap K L) (-2)) = -2
Theorem: IsPrimitiveRoot.sub_one_norm_two'
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) ((algebraMap K L) (-2)) = -2
Tactic:
rw [Algebra.norm_algebraMap, finrank_eq_one_iff'.mpr, pow_one]
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ ∃ v, v ≠ 0 ∧ ∀ (w : L), ∃ c, c • v = w
Theorem: IsPrimitiveRoot.sub_one_norm_two'
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ ∃ v, v ≠ 0 ∧ ∀ (w : L), ∃ c, c • v = w
Tactic:
refine ⟨1, one_ne_zero, fun w ↦ ?_⟩
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
w : L
⊢ ∃ c, c • 1 = w
Theorem: IsPrimitiveRoot.sub_one_norm_two'
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
w : L
⊢ ∃ c, c • 1 = w
Tactic:
simpa only [Algebra.algebraMap_eq_smul_one] using surjective_of_isCyclotomicExtension_two K L w
Proof state after:
no goals
Theorem: IsPrimitiveRoot.sub_one_norm_two'
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 : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
this : (Algebra.norm K) ((algebraMap K L) (-2)) = -2
⊢ (Algebra.norm K) (-1 - 1) = -2
Tactic:
simpa only [sub_eq_add_neg, ← one_add_one_eq_two,
  neg_add_rev, map_add, map_neg, map_one] using this
Proof state after:
no goals
Theorem: norm_Int_zeta_sub_one'
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
hp : p = 2
⊢ (Algebra.norm ℤ) (↑hζ.unit' - 1) = -↑↑p
Tactic:
clear ‹p ≠ 2›
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
⊢ (Algebra.norm ℤ) (↑hζ.unit' - 1) = -↑↑p
Theorem: norm_Int_zeta_sub_one'
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
⊢ (Algebra.norm ℤ) (↑hζ.unit' - 1) = -↑↑p
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
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Algebra.norm ℤ) (↑hζ.unit' - 1) = -↑↑p
Theorem: norm_Int_zeta_sub_one'
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
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Algebra.norm ℤ) (↑hζ.unit' - 1) = -↑↑p
Tactic:
haveI : 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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ (Algebra.norm ℤ) (↑hζ.unit' - 1) = -↑↑p
Theorem: norm_Int_zeta_sub_one'
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ (Algebra.norm ℤ) (↑hζ.unit' - 1) = -↑↑p
Tactic:
apply RingHom.injective_int (algebraMap ℤ ℚ)
Proof state after:
case a
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (↑hζ.unit' - 1)) = (algebraMap ℤ ℚ) (-↑↑p)
Theorem: norm_Int_zeta_sub_one'
Proof state before:
case a
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (↑hζ.unit' - 1)) = (algebraMap ℤ ℚ) (-↑↑p)
Tactic:
subst hp
Proof state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hpri : Fact (PNat.Prime 2)
inst✝ : IsCyclotomicExtension {2} ℚ K
hζ : IsPrimitiveRoot ζ ↑2
this✝ : NumberField K := IsCyclotomicExtension.numberField {2} ℚ K
this : Fact (↑2).Prime
⊢ (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (↑hζ.unit' - 1)) = (algebraMap ℤ ℚ) (-↑↑2)
Theorem: norm_Int_zeta_sub_one'
Proof state before:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hpri : Fact (PNat.Prime 2)
inst✝ : IsCyclotomicExtension {2} ℚ K
hζ : IsPrimitiveRoot ζ ↑2
this✝ : NumberField K := IsCyclotomicExtension.numberField {2} ℚ K
this : Fact (↑2).Prime
⊢ (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (↑hζ.unit' - 1)) = (algebraMap ℤ ℚ) (-↑↑2)
Tactic:
simp [Algebra.coe_norm_int, hζ.sub_one_norm_two']
Proof state after:
no goals
Theorem: associated_zeta_sub_one_pow_prime
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
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p
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
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p
Theorem: associated_zeta_sub_one_pow_prime
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
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p
Tactic:
haveI : 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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p
Theorem: associated_zeta_sub_one_pow_prime
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p
Tactic:
rw [← eval_one_cyclotomic_prime (R := 𝓞 K) (p := p),
  cyclotomic_eq_prod_X_sub_primitiveRoots hζ.unit'_coe, eval_prod]
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) (∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j))
Theorem: associated_zeta_sub_one_pow_prime
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) (∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j))
Tactic:
simp only [eval_sub, eval_X, eval_C]
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) (∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x))
Theorem: associated_zeta_sub_one_pow_prime
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) (∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x))
Tactic:
rw [← Nat.totient_prime this.out, ← hζ.unit'_coe.card_primitiveRoots, ← Finset.prod_const]
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated (∏ _x ∈ primitiveRoots (↑p) (𝓞 K), (↑hζ.unit' - 1)) (∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x))
Theorem: associated_zeta_sub_one_pow_prime
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated (∏ _x ∈ primitiveRoots (↑p) (𝓞 K), (↑hζ.unit' - 1)) (∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x))
Tactic:
apply Associated.prod
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ ∀ i ∈ primitiveRoots (↑p) (𝓞 K), Associated (↑hζ.unit' - 1) (1 - i)
Theorem: associated_zeta_sub_one_pow_prime
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ ∀ i ∈ primitiveRoots (↑p) (𝓞 K), Associated (↑hζ.unit' - 1) (1 - i)
Tactic:
intro η hη
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
η : 𝓞 K
hη : η ∈ primitiveRoots (↑p) (𝓞 K)
⊢ Associated (↑hζ.unit' - 1) (1 - η)
Theorem: associated_zeta_sub_one_pow_prime
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
η : 𝓞 K
hη : η ∈ primitiveRoots (↑p) (𝓞 K)
⊢ Associated (↑hζ.unit' - 1) (1 - η)
Tactic:
exact hζ.unit'_coe.associated_sub_one hpri.out
  (one_mem_nthRootsFinset this.out.pos)
  ((isPrimitiveRoot_of_mem_primitiveRoots hη).mem_nthRootsFinset hpri.out.pos)
    ((isPrimitiveRoot_of_mem_primitiveRoots hη).ne_one hpri.out.one_lt).symm
Proof state after:
no goals
Theorem: isCoprime_of_not_zeta_sub_one_dvd
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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
⊢ IsCoprime (↑↑p) x
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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ IsCoprime (↑↑p) x
Theorem: isCoprime_of_not_zeta_sub_one_dvd
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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ IsCoprime (↑↑p) x
Tactic:
rwa [← Ideal.isCoprime_span_singleton_iff,
  ← Ideal.span_singleton_eq_span_singleton.mpr (associated_zeta_sub_one_pow_prime hζ),
  ← Ideal.span_singleton_pow, IsCoprime.pow_left_iff, Ideal.isCoprime_iff_gcd,
  hζ.prime_span_sub_one.irreducible.gcd_eq_one_iff, Ideal.dvd_span_singleton,
  Ideal.mem_span_singleton]
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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ 0 < ↑p - 1
Theorem: isCoprime_of_not_zeta_sub_one_dvd
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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ 0 < ↑p - 1
Tactic:
simpa only [ge_iff_le, tsub_pos_iff_lt] using hpri.out.one_lt
Proof state after:
no goals
Theorem: exists_zeta_sub_one_dvd_sub_Int
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, ↑hζ.unit' - 1 ∣ a - ↑b
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
a : 𝓞 K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b
Theorem: exists_zeta_sub_one_dvd_sub_Int
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
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b
Tactic:
letI : 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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b
Theorem: exists_zeta_sub_one_dvd_sub_Int
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
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b
Tactic:
simp_rw [← Ideal.Quotient.eq_zero_iff_dvd, map_sub, sub_eq_zero, ← SModEq.Ideal_def]
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
⊢ ∃ b, a ≡ ↑b [SMOD Ideal.span {↑hζ.unit' - 1}]
Theorem: exists_zeta_sub_one_dvd_sub_Int
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
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
⊢ ∃ b, a ≡ ↑b [SMOD Ideal.span {↑hζ.unit' - 1}]
Tactic:
convert exists_int_sModEq hζ.subOneIntegralPowerBasis' a
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ζ.subOneIntegralPowerBasis'.gen