internlm/Lean-Github huggingface dataset:
Theorem: PowerBasis.finrank'
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✝⁴ : Module (CyclotomicIntegers ↑p) G
R : Type u_5
S : Type u_6
inst✝³ : CommRing R
inst✝² : Nontrivial R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
⊢ finrank R S = pb.dim
Tactic:
rw [FiniteDimensional.finrank_eq_card_basis pb.basis, Fintype.card_fin]
Proof state after:
no goals
Theorem: finrank_span_set_eq_card'
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✝⁵ : Module (CyclotomicIntegers ↑p) G
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card
Tactic:
have : Module.rank R (span R s) = #s := rank_span_set hs
Proof state after:
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✝⁵ : Module (CyclotomicIntegers ↑p) G
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
this : Module.rank R ↥(span R s) = #↑s
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card
Theorem: finrank_span_set_eq_card'
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✝⁵ : Module (CyclotomicIntegers ↑p) G
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
this : Module.rank R ↥(span R s) = #↑s
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card
Tactic:
rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this
Proof state after:
no goals
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Tactic:
classical
letI := Fact.mk hp
have := finrank_span_set_eq_card' (R := A) (Set.range f)
  ((linearIndependent_subtype_range hf.injective).mpr hf)
simp only [Set.toFinset_range, Finset.card_image_of_injective _ hf.injective, card_fin] at this
rw [← CyclotomicIntegers.powerBasis_dim, ← PowerBasis.finrank']
conv_rhs => rw [← this]
have := Module.Free.of_basis (Basis.span hf)
have := Module.Finite.of_basis (Basis.span hf)
rw [finrank_mul_finrank]
Proof state after:
no goals
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Tactic:
letI := Fact.mk hp
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this : Fact (↑p).Prime := { out := hp }
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this : Fact (↑p).Prime := { out := hp }
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Tactic:
have := finrank_span_set_eq_card' (R := A) (Set.range f)
  ((linearIndependent_subtype_range hf.injective).mpr hf)
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this :
  finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (Set.range f).toFinset.card
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this :
  finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (Set.range f).toFinset.card
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Tactic:
simp only [Set.toFinset_range, Finset.card_image_of_injective _ hf.injective, card_fin] at this
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Tactic:
rw [← CyclotomicIntegers.powerBasis_dim, ← PowerBasis.finrank']
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = finrank ℤ (CyclotomicIntegers ↑p) * R
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = finrank ℤ (CyclotomicIntegers ↑p) * R
Tactic:
conv_rhs => rw [← this]
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Tactic:
have := Module.Free.of_basis (Basis.span hf)
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝¹ : Fact (↑p).Prime := { out := hp }
this✝ : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
this : Module.Free (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝¹ : Fact (↑p).Prime := { out := hp }
this✝ : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
this : Module.Free (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Tactic:
have := Module.Finite.of_basis (Basis.span hf)
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝² : Fact (↑p).Prime := { out := hp }
this✝¹ : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
this✝ : Module.Free (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
this : Module.Finite (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Theorem: systemOfUnits.finrank_spanA
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝² : Fact (↑p).Prime := { out := hp }
this✝¹ : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
this✝ : Module.Free (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
this : Module.Finite (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Tactic:
rw [finrank_mul_finrank]
Proof state after:
no goals
Theorem: systemOfUnits.ex_not_mem
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
⊢ ∃ g, ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Tactic:
have := Fact.mk hp
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this : Fact (↑p).Prime
⊢ ∃ g, ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Theorem: systemOfUnits.ex_not_mem
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this : Fact (↑p).Prime
⊢ ∃ g, ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Tactic:
have : Module.Finite ℤ G := Module.finite_of_finrank_pos
  (by simp [hf, R.zero_le.trans_lt hR, hp.one_lt])
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this✝ : Fact (↑p).Prime
this : Module.Finite ℤ G
⊢ ∃ g, ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Theorem: systemOfUnits.ex_not_mem
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this✝ : Fact (↑p).Prime
this : Module.Finite ℤ G
⊢ ∃ g, ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Tactic:
refine FiniteDimensional.exists_of_finrank_lt
  ((Submodule.span A (Set.range S.units)).restrictScalars ℤ) ?_
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this✝ : Fact (↑p).Prime
this : Module.Finite ℤ G
⊢ finrank ℤ ↥(Submodule.restrictScalars ℤ (Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))) < finrank ℤ G
Theorem: systemOfUnits.ex_not_mem
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this✝ : Fact (↑p).Prime
this : Module.Finite ℤ G
⊢ finrank ℤ ↥(Submodule.restrictScalars ℤ (Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))) < finrank ℤ G
Tactic:
show finrank ℤ (Submodule.span A _) < _
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this✝ : Fact (↑p).Prime
this : Module.Finite ℤ G
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)) < finrank ℤ G
Theorem: systemOfUnits.ex_not_mem
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this✝ : Fact (↑p).Prime
this : Module.Finite ℤ G
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)) < finrank ℤ G
Tactic:
rw [finrank_spanA p hp G S.units S.linearIndependent, hf, mul_comm]
Proof state after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this✝ : Fact (↑p).Prime
this : Module.Finite ℤ G
⊢ R * (↑p - 1) < r * (↑p - 1)
Theorem: systemOfUnits.ex_not_mem
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this✝ : Fact (↑p).Prime
this : Module.Finite ℤ G
⊢ R * (↑p - 1) < r * (↑p - 1)
Tactic:
exact Nat.mul_lt_mul_of_lt_of_le hR rfl.le hp.pred_pos
Proof state after:
no goals
Theorem: systemOfUnits.ex_not_mem
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
this : Fact (↑p).Prime
⊢ 0 < finrank ℤ G
Tactic:
simp [hf, R.zero_le.trans_lt hR, hp.one_lt]
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 : ℕ
S : systemOfUnits p G R
hR : R < r
⊢ Nonempty (systemOfUnits p G (R + 1))
Tactic:
obtain ⟨g, hg⟩ := ex_not_mem p hp G r hf S hR
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)
⊢ Nonempty (systemOfUnits p G (R + 1))
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)
⊢ Nonempty (systemOfUnits p G (R + 1))
Tactic:
refine ⟨⟨Fin.cases g S.units, ?_⟩⟩
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)
⊢ LinearIndependent (CyclotomicIntegers ↑p) fun i => Fin.cases g S.units i