Theorems · Theorem · nonassociative algebras
LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero
∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [CharZero R] [IsDomain R] [inst_3 : LieRing L]
[inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : LieRingModule L M] [inst_7 : Module R M]
[inst_8 : LieModule R L M] [IsNoetherian R M] [Module.Free R M],
LieModule.traceForm R L M = 0 → LieModule.IsNilpotent (↥(LieAlgebra.derivedSeries R L 1)) MIf the trace form of M is zero, then the ⁅L, L⁆-module M is nilpotent.
- Defined in
- Mathlib.Algebra.Lie.CartanCriterion
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites37
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- LinearMapstatement · cited by 10,215
- TensorProductproof · cited by 2,545
- IsDomainstatement and proof · cited by 2,196
- LieRingstatement and proof · cited by 1,548
- LieAlgebrastatement and proof · cited by 1,246
- TensorProduct.tmulproof · cited by 1,182
- CharZerostatement and proof · cited by 932
Cited by1
Results whose statement or proof uses this declaration.
- LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zeroproof · cited by 2