internlm/Lean-Github huggingface dataset:
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
this✝⁴ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg✝ : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
hg : (Finsupp.total (Fin (r + 1)) G A S.units) ((1 - zeta ↑p) • l - a) = 0
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
hS' : S'.units ∘ i.succAbove = S.units ∘ i.succAbove
ha' :
  (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a' + S.units i =
    (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝³ : S'.IsMaximal := isMaximal p hp G hf S'
this✝² : Module A A := Algebra.toModule
this✝¹ : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
this✝ : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
this : ((1 - zeta ↑p) • ⇑l) i = 1
⊢ False
Tactic:
exact CyclotomicIntegers.not_isUnit_one_sub_zeta p
  (isUnit_of_mul_eq_one _ _ this)
Proof state after:
no goals
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
ha : ∃ i, ¬↑↑p ∣ a i
⊢ ∀ (g : G), (1 - zeta ↑p) • g ≠ ∑ i : Fin r, a i • S.units i
Tactic:
intro g hg
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
ha : ∃ i, ¬↑↑p ∣ a i
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
⊢ False
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
ha : ∃ i, ¬↑↑p ∣ a i
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
⊢ False
Tactic:
obtain ⟨i, hi⟩ := ha
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
⊢ False
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
⊢ False
Tactic:
letI := Fact.mk hp
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
⊢ False
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
⊢ False
Tactic:
obtain ⟨x, y, e⟩ := CyclotomicIntegers.isCoprime_one_sub_zeta p (a i) hi
Proof state after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
⊢ False
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
⊢ False
Tactic:
let b' : Fin r → A := fun j ↦ x * (1 - zeta ↑p) + y * (a j)
Proof state after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
⊢ False
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
⊢ False
Tactic:
let b := Finsupp.ofSupportFinite b' (Set.toFinite (Function.support _))
Proof state after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ False
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ False
Tactic:
have hb : b i = 1 := by rw [← e]; rfl
Proof state after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ False
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ False
Tactic:
apply lemma2 p hp G r hf S hs i b hb (x • ∑ i, S.units i + y • g)
Proof state after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ (1 - zeta ↑p) • (x • ∑ i : Fin r, S.units i + y • g) = (Finsupp.total (Fin r) G A S.units) b
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ (1 - zeta ↑p) • (x • ∑ i : Fin r, S.units i + y • g) = (Finsupp.total (Fin r) G A S.units) b
Tactic:
rw [smul_add, smul_smul _ y, mul_comm, ← smul_smul, hg, smul_sum, smul_sum, smul_sum,
  ← sum_add_distrib, Finsupp.total_apply, Finsupp.sum_fintype]
Proof state after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ ∑ x_1 : Fin r, ((1 - zeta ↑p) • x • S.units x_1 + y • a x_1 • S.units x_1) = ∑ i : Fin r, b i • S.units i

case intro.intro.intro.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ ∀ (i : Fin r), 0 • S.units i = 0
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ b i = 1
Tactic:
rw [← e]
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ b i = x * (1 - zeta ↑p) + y * ↑(a i)
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ b i = x * (1 - zeta ↑p) + y * ↑(a i)
Tactic:
rfl
Proof state after:
no goals
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro.intro.intro.e_f
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ (fun x_1 => (1 - zeta ↑p) • x • S.units x_1 + y • a x_1 • S.units x_1) = fun i => b i • S.units i
Tactic:
ext j
Proof state after:
case intro.intro.intro.e_f.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ (1 - zeta ↑p) • x • S.units j + y • a j • S.units j = b j • S.units j
Theorem: systemOfUnits.IsFundamental.corollary
Proof state before:
case intro.intro.intro.e_f.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ (1 - zeta ↑p) • x • S.units j + y • a j • S.units j = b j • S.units j
Tactic:
simp only [smul_smul, Finsupp.ofSupportFinite_coe, add_smul, b', b]
Proof state after:
case intro.intro.intro.e_f.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ ((1 - zeta ↑p) * x) • S.units j + y • a j • S.units j = (x * (1 - zeta ↑p)) • S.units j + (y * ↑(a j)) • S.units j