theorem LieModule.lowerCentralSeries_mono {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m n : ℕ) (h : n ≤ m) : lowerCentralSeries R L M m ≤ lowerCentralSeries R L M n

theorem LieModule.isNilpotent_iff_eventually (R : Type u_1) {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : IsNilpotent L M ↔ ∀ᶠ (k : ℕ) in Filter.atTop, lowerCentralSeries R L M k = ⊥

theorem LieModule.isNilpotent_iff_eventually_int {L : Type u_2} {M : Type u_3} [LieRing L] [AddCommGroup M] [LieRingModule L M] : IsNilpotent L M ↔ ∀ᶠ (k : ℕ) in Filter.atTop, lowerCentralSeries ℤ L M k = ⊥

theorem LieModule.isNilpotent_of_lieIdeal_le_left {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I₁ I₂ : LieIdeal R L) (h : I₁ ≤ I₂) [IsNilpotent (↥I₂) M] : IsNilpotent (↥I₁) M

theorem LieModule.isNilpotent_lieIdeal_congr_left {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I₁ I₂ : LieIdeal R L) (h : I₁ = I₂) : IsNilpotent (↥I₁) M ↔ IsNilpotent (↥I₂) M

@[simp]

theorem LieModule.isNilpotent_of_top_lieIdeal_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : IsNilpotent (↥⊤) M ↔ IsNilpotent L M

theorem LieModule.nilpotencyLength_eq_iInf (R : Type u_1) {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : nilpotencyLength L M = sInf {k : ℕ | lowerCentralSeries R L M k = ⊥}

theorem LieModule.nilpotencyLength_le_iff (R : Type u_1) {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] {n : ℕ} : nilpotencyLength L M ≤ n ↔ lowerCentralSeries R L M n = ⊥

@[simp]

theorem LieModule.lowerCentralSeries_nilpotencyLength (R : Type u_1) {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] : lowerCentralSeries R L M (nilpotencyLength L M) = ⊥

theorem LieModule.list_prod_map_toEnd_apply_mem_lowerCentralSeries (R : Type u_1) {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (l : List L) (m : M) : (List.map (⇑(toEnd R L M)) l).prod m ∈ lowerCentralSeries R L M l.length

instance LieModule.instIsNilpotentSubtypeMemLieIdeal_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) [IsNilpotent L M] : IsNilpotent (↥I) M

instance LieModule.instIsNilpotentSubtypeMemLieSubalgebra_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (L' : LieSubalgebra R L) [IsNilpotent L M] : IsNilpotent (↥L') M

instance LieModule.instIsNilpotentSubtypeMemLieSubmodule_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) [IsNilpotent L M] : IsNilpotent L ↥N