Theorems · Theorem · nonassociative algebras

LieModule.antitone_lowerCentralSeries

∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M],
  Antitone (LieModule.lowerCentralSeries R L M)

Defined in: Mathlib.Algebra.Lie.Nilpotent
Cited by: 6 results in Mathlib
Foundations: Depth 26 from the axioms · uses propext, Quot.sound
Assumes: CommRing LieRing LieAlgebra AddCommGroup Module LieRingModule

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
Top.topproof · cited by 9,680
LE.le.transproof · cited by 3,151
le_rflproof · cited by 1,558
LieRingstatement and proof · cited by 1,548
LieAlgebrastatement and proof · cited by 1,246
LieRingModulestatement and proof · cited by 727
Antitonestatement · cited by 563
LieSubmodulestatement and proof · cited by 489
LieModule.lowerCentralSeriesstatement and proof · cited by 60

Cited by6

Results whose statement or proof uses this declaration.

LieModule.nilpotencyLength_eq_succ_iffproof · cited by 3
LieModule.lowerCentralSeriesLast_le_of_not_isTrivialproof · cited by 1
LieModule.eventually_iInf_lowerCentralSeries_eqproof · cited by 1
LieSubmodule.lcs_le_lcs_of_is_nilpotent_span_sup_eq_topproof · cited by 1
LieModule.isNilpotent_toEnd_of_isNilpotent₂proof · cited by 1
LieModule.trace_toEnd_eq_zero_of_mem_lcsproof · cited by 1