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 LieRing.isNilpotent_of_lieIdeal_le {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I₁ I₂ : LieIdeal R L) (h : I₁ ≤ I₂) [IsNilpotent ↥I₂] : IsNilpotent ↥I₁

theorem LieRing.isNilpotent_of_lieSubalgebra_le {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (L' L'' : LieSubalgebra R L) (h : L' ≤ L'') [IsNilpotent ↥L''] : IsNilpotent ↥L'

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

theorem isNilpotent_lieSubalgebra_congr {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (L' L'' : LieSubalgebra R L) (h : L' = L'') : LieRing.IsNilpotent ↥L' ↔ LieRing.IsNilpotent ↥L''

@[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 LieRing.isNilpotent_lieIdeal_top_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : IsNilpotent ↥⊤ ↔ IsNilpotent L

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) (n : ℕ := l.length) (hn : n = l.length := by rfl) : (List.map (⇑(toEnd R L M)) l).prod m ∈ lowerCentralSeries R L M n

theorem LieModule.fin_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] {n : ℕ} (f : Fin n → L) (m : M) : (Fin.prod (⇑(toEnd R L M) ∘ f)) m ∈ lowerCentralSeries R L M n

theorem LieModule.isNilpotent_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] (L' L'' : LieSubalgebra R L) (h : L' = L'') : IsNilpotent (↥L') M ↔ IsNilpotent (↥L'') M

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

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

instance LieModule.instIsNilpotentSubtypeMemLieSubalgebraToLieSubalgebraOfLieIdeal_ado_1 {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRing.IsNilpotent ↥I] : LieRing.IsNilpotent ↥(↑R L I)

instance LieModule.instIsNilpotentSubtypeMemLieSubalgebraLieSubmodule_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) (N : LieSubmodule R L M) [IsNilpotent (↥L') M] : IsNilpotent ↥L' ↥N

instance LieModule.instIsNilpotentSubtypeMemLieIdealLieSubmodule_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) (N : LieSubmodule R L M) [IsNilpotent (↥I) M] : IsNilpotent ↥I ↥N

instance LieModule.isNilpotent_sup_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] (L' : LieSubalgebra R L) (I : LieIdeal R L) [IsNilpotent (↥L') M] [IsNilpotent (↥I) M] : IsNilpotent (↥(L' ⊔ ↑R L I)) M

instance LieModule.instIsNilpotentSubtypeMemLieIdealMax_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 I' : LieIdeal R L) [IsNilpotent (↥I) M] [IsNilpotent (↥I') M] : IsNilpotent (↥(I ⊔ I')) M

instance LieModule.instIsNilpotentSubtypeMemLieIdealOfIsNilpotent_ado {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRing.IsNilpotent ↥I] : IsNilpotent (↥I) L