Lie

📁 Source: Mathlib/RingTheory/Derivation/Lie.lean

Statistics

Metric	Count
Definitions mk, couple, instBracket, instLieAlgebra, instLieRing, instLieRingModule	6
Theorems apply, mem, mk_left, mk_right, bracket_eq_fun, commutator_apply, commutator_coe_linear_map, instLieModule	8
Total	14

Derivation

Definitions

Name	Category	Theorems
couple 📖	CompOp	4 math math: Compatible.mem, Compatible.apply, Compatible.mk_left, Compatible.mk_right
instBracket 📖	CompOp	3 math math: commutator_coe_linear_map, commutator_apply, LeftInvariantDerivation.commutator_coe_derivation
instLieAlgebra 📖	CompOp	9 math math: instLieModule, LieRinehartAlgebra.anchor_apply, Compatible.mem, Compatible.apply, LieRinehartAlgebra.anchor_derivation, Lie.Derivation.ofDerivation_apply, LieRinehartAlgebra.instDerivation, Compatible.mk_left, Compatible.mk_right
instLieRing 📖	CompOp	11 math math: bracket_eq_fun, instLieModule, LieRinehartAlgebra.anchor_apply, Compatible.mem, Compatible.apply, LieRinehartAlgebra.anchor_derivation, Lie.Derivation.ofDerivation_apply, LieRinehartAlgebra.instDerivation, Compatible.mk_left, Compatible.mk_right, LieRinehartAlgebra.instLieRinehartRingDerivation
instLieRingModule 📖	CompOp	6 math math: bracket_eq_fun, instLieModule, LieRinehartAlgebra.anchor_apply, LieRinehartAlgebra.anchor_derivation, LieRinehartAlgebra.instDerivation, LieRinehartAlgebra.instLieRinehartRingDerivation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bracket_eq_fun 📖	mathematical	—	Bracket.bracket Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id LieRingModule.toBracket instLieRing LieRing.toAddCommGroup instLieRingModule DFunLike.coe instFunLike	—	—
commutator_apply 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id instFunLike Bracket.bracket instBracket SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—
commutator_coe_linear_map 📖	mathematical	—	toLinearMap CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Bracket.bracket Derivation instBracket LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LieRingModule.toBracket Module.End.instRing LieRing.toAddCommGroup LinearMap.addCommGroup AddCommGroup.toAddCommMonoid LinearMap.instLieRingModule Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.End.instLieRingModule Module.End.instLieModule	—	—
instLieModule 📖	mathematical	—	LieModule Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id instLieRing instLieAlgebra LieRing.toAddCommGroup instLieRingModule	—	map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul IsScalarTower.left

Derivation.Compatible

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Derivation.instFunLike LieSubalgebra LieAlgebra.Prod.instLieRing Derivation.instLieRing LieAlgebra.Prod.instLieAlgebra Derivation.instLieAlgebra SetLike.instMembership LieSubalgebra.instSetLike Derivation.couple AlgHom CommSemiring.toSemiring AlgHom.funLike Algebra.ofId	—	—
mem 📖	mathematical	—	Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id LieSubalgebra LieAlgebra.Prod.instLieRing Derivation.instLieRing LieAlgebra.Prod.instLieAlgebra Derivation.instLieAlgebra SetLike.instMembership LieSubalgebra.instSetLike Derivation.couple DFunLike.coe Derivation.instFunLike AlgHom CommSemiring.toSemiring AlgHom.funLike Algebra.ofId	—	Derivation.ext
mk_left 📖	mathematical	DFunLike.coe Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Derivation.instFunLike AlgHom CommSemiring.toSemiring AlgHom.funLike Algebra.ofId	Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id LieSubalgebra LieAlgebra.Prod.instLieRing Derivation.instLieRing LieAlgebra.Prod.instLieAlgebra Derivation.instLieAlgebra SetLike.instMembership LieSubalgebra.instSetLike Derivation.couple	—	—
mk_right 📖	mathematical	DFunLike.coe Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Derivation.instFunLike AlgHom CommSemiring.toSemiring AlgHom.funLike Algebra.ofId	Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id LieSubalgebra LieAlgebra.Prod.instLieRing Derivation.instLieRing LieAlgebra.Prod.instLieAlgebra Derivation.instLieAlgebra SetLike.instMembership LieSubalgebra.instSetLike Derivation.couple	—	—

---

← Back to Index