Theorems · Theorem · nonassociative algebras
trivial_lie_zero
∀ (L : Type v) (M : Type w) [inst : Bracket L M] [inst_1 : Zero M] [LieModule.IsTrivial L M] (x : L) (m : M), ⁅x, m⁆ = 0
- Defined in
- Mathlib.Algebra.Lie.Abelian
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bracket.bracketstatement · cited by 642
- LieModule.IsTrivialstatement and proof · cited by 14
- Bracketstatement and proof · cited by 8
- LieModule.IsTrivial.trivialproof · cited by 6
Cited by13
Results whose statement or proof uses this declaration.
- LieAlgebra.Extension.lieModuleOfproof · cited by 3
- LieSubmodule.trivial_lie_oper_zeroproof · cited by 3
- Function.Injective.isLieAbelianproof · cited by 2
- LieAlgebra.IsKilling.corootSpace_zero_eq_botproof · cited by 2
- LieAlgebra.Extension.ringModuleOf_bracket_projproof · cited by 1
- LieSubalgebra.isLieAbelian_lieSpan_iffproof · cited by 1
- LieAlgebra.IsKilling.eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebraproof · cited by 1
- LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplittingproof · cited by 0
- Function.Surjective.isLieAbelianproof · cited by 0
- LieModule.Cohomology.d₁₂_apply_apply_ofTrivialproof · cited by 0
- LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eqproof · cited by 0
- LieModule.Cohomology.mem_twoCocycle_iff_of_trivialproof · cited by 0