Theorem: systemOfUnits.ex_not_mem (FltRegular/NumberTheory/SystemOfUnits.lean)

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
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)

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])
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)

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 ℤ) ?_
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

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 _) < _
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

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]
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)

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
State after:
no goals

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]
State after:
no goals