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
⊢ ∑ 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
Tactic:
congr
Proof state after:
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

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