Theorems · Inductive type · nonassociative algebras
LieModule.IsTrivial
(L : Type v) → (M : Type w) → [Bracket L M] → [Zero M] → Prop
A Lie (ring) module is trivial iff all brackets vanish.
- Defined in
- Mathlib.Algebra.Lie.Abelian
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bracketstatement · cited by 8
Cited by17
Results whose statement or proof uses this declaration.
- IsLieAbelianproof · cited by 55
- trivial_lie_zerostatement and proof · cited by 13
- LieModule.IsTrivial.trivialstatement and proof · cited by 6
- LieSubmodule.trivial_lie_oper_zerostatement and proof · cited by 3
- LieModule.IsTrivial.casesOnstatement and proof · cited by 2
- LieModule.trivial_iff_lower_central_eq_botstatement and proof · cited by 1
- LieModule.isTrivial_iff_max_triv_eq_topstatement and proof · cited by 1
- LieModule.isTrivial_of_nilpotencyLength_le_onestatement · cited by 1
- LieSubmodule.traceForm_eq_zero_of_isTrivialstatement and proof · cited by 1
- LieModule.lowerCentralSeriesLast_le_of_not_isTrivialstatement and proof · cited by 1
- LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iffstatement and proof · cited by 1
- LieModule.nilpotencyLength_eq_one_iffstatement and proof · cited by 1