internlm/Lean-Github huggingface dataset:
Theorem: systemOfUnits.existence'
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
⊢ LinearIndependent (CyclotomicIntegers ↑p) fun i => Fin.cases g S.units i
Tactic:
refine LinearIndependent.fin_cons' g S.units S.linearIndependent (fun a y hy ↦ ?_)
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
⊢ a = 0
Theorem: systemOfUnits.existence'
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
⊢ a = 0
Tactic:
by_contra! ha
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
⊢ False
Theorem: systemOfUnits.existence'
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
⊢ False
Tactic:
letI := Fact.mk hp
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
⊢ False
Theorem: systemOfUnits.existence'
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
⊢ False
Tactic:
obtain ⟨n, h0, f, Hf⟩ := CyclotomicIntegers.exists_dvd_int p _ ha
Proof state after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
⊢ False
Theorem: systemOfUnits.existence'
Proof state before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : (fun x => f • x) (a • g + ↑y) = (fun x => f • x) 0
⊢ False
Tactic:
simp only at hy
Proof state after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : f • (a • g + ↑y) = f • 0
⊢ False
Theorem: systemOfUnits.existence'
Proof state before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : f • (a • g + ↑y) = f • 0
⊢ False
Tactic:
rw [smul_zero, smul_add, smul_smul, mul_comm f,
  ← Hf, ← eq_neg_iff_add_eq_zero, intCast_smul] at hy
Proof state after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ False
Theorem: systemOfUnits.existence'
Proof state before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ False
Tactic:
apply hg _ h0
Proof state after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ n • g ∈ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Theorem: systemOfUnits.existence'
Proof state before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ n • g ∈ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Tactic:
rw [hy]
Proof state after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ -(f • ↑y) ∈ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Theorem: systemOfUnits.existence'
Proof state before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ -(f • ↑y) ∈ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Tactic:
exact Submodule.neg_mem _ (Submodule.smul_mem _ _ y.2)
Proof state after:
no goals
Theorem: systemOfUnits.existence''
Proof state before:
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
hR : R ≤ r
⊢ Nonempty (systemOfUnits p G R)
Tactic:
induction R with
| zero => exact existence0 p G
| succ n ih =>
    obtain ⟨S⟩ := ih (le_trans (Nat.le_succ n) hR)
    exact existence' p hp G r hf S (lt_of_lt_of_le (Nat.lt.base n) hR)
Proof state after:
no goals
Theorem: systemOfUnits.existence''
Proof state before:
case zero
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
hR : 0 ≤ r
⊢ Nonempty (systemOfUnits p G 0)
Tactic:
exact existence0 p G
Proof state after:
no goals
Theorem: systemOfUnits.existence''
Proof state before:
case succ
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
n : ℕ
ih : n ≤ r → Nonempty (systemOfUnits p G n)
hR : n + 1 ≤ r
⊢ Nonempty (systemOfUnits p G (n + 1))
Tactic:
obtain ⟨S⟩ := ih (le_trans (Nat.le_succ n) hR)
Proof state after:
case succ.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
n : ℕ
ih : n ≤ r → Nonempty (systemOfUnits p G n)
hR : n + 1 ≤ r
S : systemOfUnits p G n
⊢ Nonempty (systemOfUnits p G (n + 1))
Theorem: systemOfUnits.existence''
Proof state before:
case succ.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
n : ℕ
ih : n ≤ r → Nonempty (systemOfUnits p G n)
hR : n + 1 ≤ r
S : systemOfUnits p G n
⊢ Nonempty (systemOfUnits p G (n + 1))
Tactic:
exact existence' p hp G r hf S (lt_of_lt_of_le (Nat.lt.base n) hR)
Proof state after:
no goals
Theorem: IsPrimitiveRoot.prime_span_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
⊢ Prime (Ideal.span {↑hζ.unit' - 1})
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 : Fact (↑p).Prime
⊢ Prime (Ideal.span {↑hζ.unit' - 1})
Theorem: IsPrimitiveRoot.prime_span_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 : Fact (↑p).Prime
⊢ Prime (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
this✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Prime (Ideal.span {↑hζ.unit' - 1})
Theorem: IsPrimitiveRoot.prime_span_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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Prime (Ideal.span {↑hζ.unit' - 1})
Tactic:
rw [Ideal.prime_iff_isPrime,
  Ideal.span_singleton_prime (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)]
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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Prime (↑hζ.unit' - 1)

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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Ideal.span {↑hζ.unit' - 1} ≠ ⊥
Theorem: IsPrimitiveRoot.prime_span_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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Prime (↑hζ.unit' - 1)

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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Ideal.span {↑hζ.unit' - 1} ≠ ⊥
Tactic:
exact hζ.zeta_sub_one_prime'
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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Ideal.span {↑hζ.unit' - 1} ≠ ⊥
Theorem: IsPrimitiveRoot.prime_span_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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Ideal.span {↑hζ.unit' - 1} ≠ ⊥
Tactic:
rw [Ne, Ideal.span_singleton_eq_bot]
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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ¬↑hζ.unit' - 1 = 0
Theorem: IsPrimitiveRoot.prime_span_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✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ¬↑hζ.unit' - 1 = 0
Tactic:
exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt
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
⊢ (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:
simp [Algebra.coe_norm_int, hζ.norm_sub_one_of_prime_ne_two' (cyclotomic.irreducible_rat p.2) hp]
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
⊢ Function.Surjective ⇑(algebraMap R S)
Tactic:
intro x
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
⊢ ∃ 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
⊢ ∃ a, (algebraMap R S) a = x
Tactic:
have := IsCyclotomicExtension.adjoin_roots (S := {2}) (A := R) (B := S) x
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 | ∃ n ∈ {2}, b ^ ↑n = 1}
⊢ ∃ a, (algebraMap R S) a = x