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✝ N : LieSubmodule R L M
⊢ (∃ k, lowerCentralSeries R L { x // x ∈ ↑N } k = ⊥) ↔ ∃ k, LieSubmodule.lcs k N = ⊥
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✝ N : LieSubmodule R L M
⊢ IsNilpotent R L { x // x ∈ ↑N } ↔ ∃ k, LieSubmodule.lcs k N = ⊥
rw [isNilpotent_iff]
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✝ N : LieSubmodule R L M
k : ℕ
⊢ lowerCentralSeries R L { x // x ∈ ↑N } k = ⊥ ↔ LieSubmodule.lcs k N = ⊥
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✝ N : LieSubmodule R L M
⊢ (∃ k, lowerCentralSeries R L { x // x ∈ ↑N } k = ⊥) ↔ ∃ k, LieSubmodule.lcs k N = ⊥
refine' exists_congr fun k => _
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✝ N : LieSubmodule R L M
k : ℕ
⊢ lowerCentralSeries R L { x // x ∈ ↑N } k = ⊥ ↔ LieSubmodule.lcs k N = ⊥
rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot,
  inf_eq_right.mpr (N.lcs_le_self k)]