Theorem: systemOfUnits.nontrivial (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
hr : r ≠ 0
⊢ Nontrivial G
Tactic:
by_contra! h
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
hr : r ≠ 0
h : ¬Nontrivial G
⊢ False

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
hr : r ≠ 0
h : ¬Nontrivial G
⊢ False
Tactic:
rw [not_nontrivial_iff_subsingleton] at h
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
hr : r ≠ 0
h : Subsingleton G
⊢ False

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
hr : r ≠ 0
h : Subsingleton G
⊢ False
Tactic:
rw [FiniteDimensional.finrank_zero_of_subsingleton] at hf
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 : 0 = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
⊢ False

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 : 0 = r * (↑p - 1)
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
⊢ False
Tactic:
simp only [ge_iff_le, zero_eq_mul, tsub_eq_zero_iff_le] at hf
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
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
hf : r = 0 ∨ ↑p ≤ 1
⊢ False

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
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h : Subsingleton G
hf : r = 0 ∨ ↑p ≤ 1
⊢ False
Tactic:
cases hf with
| inl h => exact hr h
| inr h => simpa [Nat.lt_succ_iff, h] using not_lt.2 (Nat.prime_def_lt.1 hp).1
State after:
no goals

State before:
case inl
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
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h✝ : Subsingleton G
h : r = 0
⊢ False
Tactic:
exact hr h
State after:
no goals

State before:
case inr
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
inst✝ : Module (CyclotomicIntegers ↑p) G
hr : r ≠ 0
h✝ : Subsingleton G
h : ↑p ≤ 1
⊢ False
Tactic:
simpa [Nat.lt_succ_iff, h] using not_lt.2 (Nat.prime_def_lt.1 hp).1
State after:
no goals