Structures · Algebra
LieModule.IsTrivial
A Lie (ring) module is trivial iff all brackets vanish.
- Defined in
- Mathlib.Algebra.Lie.Abelian
- Shape
- 2 explicit arguments · adds trivial
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- trivial_lie_zero
- LieModule.IsTrivial.trivial
- LieSubmodule.trivial_lie_oper_zero
- LieSubmodule.traceForm_eq_zero_of_isTrivial
- LieIdeal.isLieAbelian_of_trivial
- LieModule.Cohomology.mem_twoCocycle_iff_of_trivial
- LieModule.traceForm_eq_zero_of_isTrivial
- LieModule.Cohomology.d₁₂_apply_apply_ofTrivial
- LieModule.trivialIsNilpotent
Ancestors0
No ancestors.