NonUnitalNonAssocAlgebra

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

Statistics

Metric	Count
Definitions CommutatorRing, instCommutatorRing, instInhabitedCommutatorRing, instLieRingCommutatorRing, toNonUnitalAlgHom, instNonUnitalNonAssocRingCommutatorRing	6
Theorems instNonemptyCommutatorRing, isScalarTower, smulCommClass, toNonUnitalAlgHom_apply, toNonUnitalAlgHom_injective, toNonUnitalAlgHom_toFun	6
Total	12

LieAlgebra

Definitions

Name	Category	Theorems
instCommutatorRing 📖	CompOp	9 math math: FreeLieAlgebra.liftAux_map_smul, FreeLieAlgebra.liftAux_map_add, LieHom.toNonUnitalAlgHom_toFun, FreeLieAlgebra.liftAux_map_mul, smulCommClass, FreeLieAlgebra.liftAux_spec, LieHom.toNonUnitalAlgHom_apply, isScalarTower, LieHom.toNonUnitalAlgHom_injective
instInhabitedCommutatorRing 📖	CompOp	—
instLieRingCommutatorRing 📖	CompOp	9 math math: FreeLieAlgebra.liftAux_map_smul, FreeLieAlgebra.liftAux_map_add, LieHom.toNonUnitalAlgHom_toFun, FreeLieAlgebra.liftAux_map_mul, smulCommClass, FreeLieAlgebra.liftAux_spec, LieHom.toNonUnitalAlgHom_apply, isScalarTower, LieHom.toNonUnitalAlgHom_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonemptyCommutatorRing 📖	mathematical	—	CommutatorRing	—	—
isScalarTower 📖	mathematical	—	IsScalarTower CommutatorRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup instLieRingCommutatorRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instNonUnitalNonAssocRingCommutatorRing toModule instCommutatorRing instDistribSMul	—	smul_lie lieAlgebraSelfModule
smulCommClass 📖	mathematical	—	SMulCommClass CommutatorRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup instLieRingCommutatorRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instNonUnitalNonAssocRingCommutatorRing toModule instCommutatorRing instDistribSMul	—	lie_smul lieAlgebraSelfModule

LieHom

Definitions

Name	Category	Theorems
toNonUnitalAlgHom 📖	CompOp	3 math math: toNonUnitalAlgHom_toFun, toNonUnitalAlgHom_apply, toNonUnitalAlgHom_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNonUnitalAlgHom_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommutatorRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instNonUnitalNonAssocRingCommutatorRing Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid LieAlgebra.toModule LieAlgebra.instLieRingCommutatorRing LieAlgebra.instCommutatorRing NonUnitalAlgHom.instFunLike toNonUnitalAlgHom LieHom instFunLike	—	—
toNonUnitalAlgHom_injective 📖	mathematical	—	LieHom NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommutatorRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instNonUnitalNonAssocRingCommutatorRing Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid LieAlgebra.toModule LieAlgebra.instLieRingCommutatorRing LieAlgebra.instCommutatorRing toNonUnitalAlgHom	—	ext NonUnitalAlgHom.congr_fun
toNonUnitalAlgHom_toFun 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommutatorRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instNonUnitalNonAssocRingCommutatorRing Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid LieAlgebra.toModule LieAlgebra.instLieRingCommutatorRing LieAlgebra.instCommutatorRing NonUnitalAlgHom.instFunLike toNonUnitalAlgHom LieHom instFunLike	—	—

(root)

Definitions

Name	Category	Theorems
CommutatorRing 📖	CompOp	10 math math: FreeLieAlgebra.liftAux_map_smul, FreeLieAlgebra.liftAux_map_add, LieHom.toNonUnitalAlgHom_toFun, FreeLieAlgebra.liftAux_map_mul, LieAlgebra.smulCommClass, LieAlgebra.instNonemptyCommutatorRing, FreeLieAlgebra.liftAux_spec, LieHom.toNonUnitalAlgHom_apply, LieAlgebra.isScalarTower, LieHom.toNonUnitalAlgHom_injective
instNonUnitalNonAssocRingCommutatorRing 📖	CompOp	9 math math: FreeLieAlgebra.liftAux_map_smul, FreeLieAlgebra.liftAux_map_add, LieHom.toNonUnitalAlgHom_toFun, FreeLieAlgebra.liftAux_map_mul, LieAlgebra.smulCommClass, FreeLieAlgebra.liftAux_spec, LieHom.toNonUnitalAlgHom_apply, LieAlgebra.isScalarTower, LieHom.toNonUnitalAlgHom_injective

---

← Back to Index