Graded

📁 Source: Mathlib/Algebra/Lie/Graded.lean

Statistics

Metric	Count
Definitions decomposeLieEquiv, instLieAlgebraSubtypeMemSubmodule, instLieRingSubtypeMemSubmodule, GradedLieAlgebra, toDecomposition, ofGrading, ofGradingSum, GradedBracket	8
Theorems bracket_apply_apply, decompose_bracket, decompose_symm_bracket, toGradedBracket, ofGradingSum_of, ofGrading_apply_apply, bracket_mem	7
Total	15

DirectSum

Definitions

Name	Category	Theorems
decomposeLieEquiv 📖	CompOp	—
instLieAlgebraSubtypeMemSubmodule 📖	CompOp	1 math math: LieDerivation.ofGradingSum_of
instLieRingSubtypeMemSubmodule 📖	CompOp	4 math math: bracket_apply_apply, LieDerivation.ofGradingSum_of, decompose_symm_bracket, decompose_bracket

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bracket_apply_apply 📖	mathematical	—	Bracket.bracket DirectSum Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid LieRingModule.toBracket instLieRingSubtypeMemSubmodule lieRingSelfModule DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instAddCommMonoidDirectSum instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv decomposeLinearEquiv GradedLieAlgebra.toDecomposition LinearEquiv.symm	—	—
decompose_bracket 📖	mathematical	—	DFunLike.coe Equiv DirectSum Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule SetLike.instMembership Submodule.setLike AddSubmonoidClass.toAddCommMonoid Submodule.addSubmonoidClass EquivLike.toFunLike Equiv.instEquivLike decompose GradedLieAlgebra.toDecomposition Bracket.bracket LieRingModule.toBracket lieRingSelfModule instLieRingSubtypeMemSubmodule	—	Submodule.addSubmonoidClass RingHomInvPair.ids LinearEquiv.symm_apply_apply
decompose_symm_bracket 📖	mathematical	—	DFunLike.coe Equiv DirectSum Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule SetLike.instMembership Submodule.setLike AddSubmonoidClass.toAddCommMonoid Submodule.addSubmonoidClass EquivLike.toFunLike Equiv.instEquivLike Equiv.symm decompose GradedLieAlgebra.toDecomposition Bracket.bracket Submodule.addCommMonoid LieRingModule.toBracket instLieRingSubtypeMemSubmodule lieRingSelfModule	—	Submodule.addSubmonoidClass RingHomInvPair.ids LinearEquiv.symm_apply_apply

GradedLieAlgebra

Definitions

Name	Category	Theorems
toDecomposition 📖	CompOp	3 math math: DirectSum.bracket_apply_apply, DirectSum.decompose_symm_bracket, DirectSum.decompose_bracket

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toGradedBracket 📖	mathematical	—	SetLike.GradedBracket Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.setLike LieRingModule.toBracket lieRingSelfModule AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—

LieDerivation

Definitions

Name	Category	Theorems
ofGrading 📖	CompOp	1 math math: ofGrading_apply_apply
ofGradingSum 📖	CompOp	1 math math: ofGradingSum_of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofGradingSum_of 📖	mathematical	—	DFunLike.coe LieDerivation DirectSum Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid DirectSum.instLieRingSubtypeMemSubmodule DirectSum.instLieAlgebraSubtypeMemSubmodule DirectSum.instAddCommGroup Submodule.addCommGroup CommRing.toRing DirectSum.instModule Submodule.module lieRingSelfModule lieAlgebraSelfModule instFunLike ofGradingSum AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike DirectSum.of SMulZeroClass.toSMul AddZero.toZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	lieAlgebraSelfModule smulCommClass_self DirectSum.toModule_lof map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
ofGrading_apply_apply 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule SetLike.instMembership Submodule.setLike	DFunLike.coe LieDerivation LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule instFunLike ofGrading SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddMonoidHom AddCommMonoid.toAddMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AddMonoidHom.instFunLike	—	lieAlgebraSelfModule Submodule.addSubmonoidClass DirectSum.decompose_of_mem ofGradingSum_of map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass DirectSum.decompose_symm_of

SetLike

Definitions

Name	Category	Theorems
GradedBracket 📖	CompData	1 math math: GradedLieAlgebra.toGradedBracket

SetLike.GradedBracket

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bracket_mem 📖	mathematical	SetLike.instMembership	SetLike.instMembership Bracket.bracket	—	—

(root)

Definitions

Name	Category	Theorems
GradedLieAlgebra 📖	CompData	—

---

← Back to Index