R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ nilpotencyLength R L M = 0 ↔ Subsingleton M
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
⊢ nilpotencyLength R L M = 0 ↔ Subsingleton M
let s := {k | lowerCentralSeries R L M k = ⊥}
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ nilpotencyLength R L M = 0 ↔ Subsingleton M
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ nilpotencyLength R L M = 0 ↔ Subsingleton M
have hs : s.Nonempty := by
  obtain ⟨k, hk⟩ := (by infer_instance : IsNilpotent R L M)
  exact ⟨k, hk⟩
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ sInf s = 0 ↔ Subsingleton M
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ nilpotencyLength R L M = 0 ↔ Subsingleton M
change sInf s = 0 ↔ _
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ sInf s = 0 ↔ lowerCentralSeries R L M 0 = ⊥
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ sInf s = 0 ↔ Subsingleton M
rw [← LieSubmodule.subsingleton_iff R L M, ← subsingleton_iff_bot_eq_top, ←
  lowerCentralSeries_zero, @eq_comm (LieSubmodule R L M)]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
h : lowerCentralSeries R L M 0 = ⊥
⊢ sInf s = 0
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ sInf s = 0 ↔ lowerCentralSeries R L M 0 = ⊥
refine' ⟨fun h => h ▸ Nat.sInf_mem hs, fun h => _⟩
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
h : lowerCentralSeries R L M 0 = ⊥
⊢ 0 ∈ s ∨ s = ∅
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
h : lowerCentralSeries R L M 0 = ⊥
⊢ sInf s = 0
rw [Nat.sInf_eq_zero]
no goals
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
h : lowerCentralSeries R L M 0 = ⊥
⊢ 0 ∈ s ∨ s = ∅
exact Or.inl h
case mk.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ Set.Nonempty s
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ Set.Nonempty s
obtain ⟨k, hk⟩ := (by infer_instance : IsNilpotent R L M)
no goals
case mk.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ Set.Nonempty s
exact ⟨k, hk⟩
no goals
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ IsNilpotent R L M
infer_instance