Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/NonAssoc/LieAdmissible/Defs.lean

Statistics

Metric	Count
Definitions `instLieAdmissibleAlgebra`, `instLieAdmissibleRing`, `LieAdmissibleAlgebra`, `instLieAlgebra`, `toModule`, `LieAdmissibleRing`, `instLieRing`, `toNonUnitalNonAssocRing`, `instLieAdmissibleAlgebra`, `instLieAdmissibleRing`	10
Theorems `ext`, `ext_iff`, `toIsScalarTower`, `toSMulCommClass`, `assoc_def`, `ext`, `ext_iff`	7
Total	17

LeftPreLieAlgebra

Definitions

Name	Category	Theorems
`instLieAdmissibleAlgebra` 📖	CompOp	—

LeftPreLieRing

Definitions

Name	Category	Theorems
`instLieAdmissibleRing` 📖	CompOp	—

LieAdmissibleAlgebra

Definitions

Name	Category	Theorems
`instLieAlgebra` 📖	CompOp	—
`toModule` 📖	CompOp	3 math math: `toSMulCommClass`, `toIsScalarTower`, `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` `LieAdmissibleRing.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` `LieAdmissibleRing.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` `LieAdmissibleRing.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` `LieAdmissibleRing.toNonUnitalNonAssocRing` `Module.toDistribMulAction` `toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul`	—	—

LieAdmissibleRing

Definitions

Name	Category	Theorems
`instLieRing` 📖	CompOp	—
`toNonUnitalNonAssocRing` 📖	CompOp	5 math math: `LieAdmissibleAlgebra.toSMulCommClass`, `ext_iff`, `LieAdmissibleAlgebra.toIsScalarTower`, `assoc_def`, `LieAdmissibleAlgebra.ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc_def` 📖	mathematical	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `toNonUnitalNonAssocRing` `associator`	—	—
`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
`instLieAdmissibleAlgebra` 📖	CompOp	—

RightPreLieRing

Definitions

Name	Category	Theorems
`instLieAdmissibleRing` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`LieAdmissibleAlgebra` 📖	CompData	—
`LieAdmissibleRing` 📖	CompData	—

---

← Back to Index