Basic

📁 Source: Mathlib/Algebra/NonAssoc/PreLie/Basic.lean

Statistics

Metric	Count
Definitions LeftPreLieAlgebra, instRightPreLieAlgebraMulOpposite, toModule, LeftPreLieRing, instRightPreLieRingMulOpposite, toNonUnitalNonAssocRing, RightPreLieAlgebra, instLeftPreLieAlgebraMulOpposite, toModule, RightPreLieRing, instLeftPreLieRingMulOpposite, toNonUnitalNonAssocRing	12
Theorems ext, ext_iff, toIsScalarTower, toSMulCommClass, assoc_symm, assoc_symm', ext, ext_iff, ext, ext_iff, toIsScalarTower, toSMulCommClass, assoc_symm, assoc_symm', ext, ext_iff	16
Total	28

LeftPreLieAlgebra

Definitions

Name	Category	Theorems
instRightPreLieAlgebraMulOpposite 📖	CompOp	—
toModule 📖	CompOp	3 math math: toSMulCommClass, ext_iff, toIsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring LeftPreLieRing.toNonUnitalNonAssocRing Module.toDistribMulAction toModule	—	—	—
ext_iff 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring LeftPreLieRing.toNonUnitalNonAssocRing Module.toDistribMulAction toModule	—	ext
toIsScalarTower 📖	mathematical	—	IsScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring LeftPreLieRing.toNonUnitalNonAssocRing Module.toDistribMulAction toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul	—	—
toSMulCommClass 📖	mathematical	—	SMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring LeftPreLieRing.toNonUnitalNonAssocRing Module.toDistribMulAction toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul	—	—

LeftPreLieRing

Definitions

Name	Category	Theorems
instRightPreLieRingMulOpposite 📖	CompOp	—
toNonUnitalNonAssocRing 📖	CompOp	6 math math: LeftPreLieAlgebra.toSMulCommClass, assoc_symm', assoc_symm, LeftPreLieAlgebra.ext_iff, ext_iff, LeftPreLieAlgebra.toIsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc_symm 📖	mathematical	—	associator toNonUnitalNonAssocRing	—	assoc_symm'
assoc_symm' 📖	mathematical	—	associator toNonUnitalNonAssocRing	—	—
ext 📖	—	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup toNonUnitalNonAssocRing AddMonoid.toZero AddMonoid.nsmul SubNegMonoid.toNeg SubNegMonoid.toSub SubNegMonoid.zsmul NonUnitalNonAssocRing.toMul	—	—	—
ext_iff 📖	mathematical	—	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup toNonUnitalNonAssocRing AddMonoid.toZero AddMonoid.nsmul SubNegMonoid.toNeg SubNegMonoid.toSub SubNegMonoid.zsmul NonUnitalNonAssocRing.toMul	—	ext

RightPreLieAlgebra

Definitions

Name	Category	Theorems
instLeftPreLieAlgebraMulOpposite 📖	CompOp	—
toModule 📖	CompOp	3 math math: toIsScalarTower, toSMulCommClass, ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring RightPreLieRing.toNonUnitalNonAssocRing Module.toDistribMulAction toModule	—	—	—
ext_iff 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring RightPreLieRing.toNonUnitalNonAssocRing Module.toDistribMulAction toModule	—	ext
toIsScalarTower 📖	mathematical	—	IsScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring RightPreLieRing.toNonUnitalNonAssocRing Module.toDistribMulAction toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul	—	—
toSMulCommClass 📖	mathematical	—	SMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring RightPreLieRing.toNonUnitalNonAssocRing Module.toDistribMulAction toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul	—	—

RightPreLieRing

Definitions

Name	Category	Theorems
instLeftPreLieRingMulOpposite 📖	CompOp	—
toNonUnitalNonAssocRing 📖	CompOp	6 math math: RightPreLieAlgebra.toIsScalarTower, RightPreLieAlgebra.toSMulCommClass, assoc_symm', assoc_symm, ext_iff, RightPreLieAlgebra.ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc_symm 📖	mathematical	—	associator toNonUnitalNonAssocRing	—	assoc_symm'
assoc_symm' 📖	mathematical	—	associator toNonUnitalNonAssocRing	—	—
ext 📖	—	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup toNonUnitalNonAssocRing AddMonoid.toZero AddMonoid.nsmul SubNegMonoid.toNeg SubNegMonoid.toSub SubNegMonoid.zsmul NonUnitalNonAssocRing.toMul	—	—	—
ext_iff 📖	mathematical	—	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup toNonUnitalNonAssocRing AddMonoid.toZero AddMonoid.nsmul SubNegMonoid.toNeg SubNegMonoid.toSub SubNegMonoid.zsmul NonUnitalNonAssocRing.toMul	—	ext

(root)

Definitions

Name	Category	Theorems
LeftPreLieAlgebra 📖	CompData	—
LeftPreLieRing 📖	CompData	—
RightPreLieAlgebra 📖	CompData	—
RightPreLieRing 📖	CompData	—

---

← Back to Index