FreeNonUnitalNonAssocAlgebra

📁 Source: Mathlib/Algebra/FreeNonUnitalNonAssocAlgebra.lean

Statistics

Metric	Count
Definitions FreeNonUnitalNonAssocAlgebra, of	2
Theorems hom_ext, hom_ext_iff, lift_comp_of, lift_of_apply, lift_symm_apply, lift_unique, of_comp_lift	7
Total	9

FreeNonUnitalNonAssocAlgebra

Definitions

Name	Category	Theorems
of 📖	CompOp	6 math math: of_comp_lift, lift_unique, lift_symm_apply, lift_of_apply, hom_ext_iff, lift_comp_of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring FreeNonUnitalNonAssocAlgebra MonoidAlgebra.nonUnitalNonAssocSemiring FreeMagma FreeMagma.instMul MonoidAlgebra.distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike_1 of	—	—	Equiv.injective
hom_ext_iff 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring FreeNonUnitalNonAssocAlgebra MonoidAlgebra.nonUnitalNonAssocSemiring FreeMagma FreeMagma.instMul MonoidAlgebra.distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike_1 of	—	hom_ext
lift_comp_of 📖	mathematical	—	DFunLike.coe Equiv NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring FreeNonUnitalNonAssocAlgebra MonoidAlgebra.nonUnitalNonAssocSemiring FreeMagma FreeMagma.instMul MonoidAlgebra.distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule EquivLike.toFunLike Equiv.instEquivLike lift NonUnitalAlgHom.instFunLike_1 of	—	Equiv.apply_symm_apply
lift_of_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring FreeNonUnitalNonAssocAlgebra MonoidAlgebra.nonUnitalNonAssocSemiring FreeMagma FreeMagma.instMul MonoidAlgebra.distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike_1 Equiv EquivLike.toFunLike Equiv.instEquivLike lift of	—	of_comp_lift
lift_symm_apply 📖	mathematical	—	DFunLike.coe Equiv NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring FreeNonUnitalNonAssocAlgebra MonoidAlgebra.nonUnitalNonAssocSemiring FreeMagma FreeMagma.instMul MonoidAlgebra.distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift NonUnitalAlgHom.instFunLike_1 of	—	—
lift_unique 📖	mathematical	—	FreeNonUnitalNonAssocAlgebra DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidAlgebra.nonUnitalNonAssocSemiring FreeMagma FreeMagma.instMul MonoidAlgebra.distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike_1 of Equiv EquivLike.toFunLike Equiv.instEquivLike lift	—	Equiv.symm_apply_eq
of_comp_lift 📖	mathematical	—	FreeNonUnitalNonAssocAlgebra DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidAlgebra.nonUnitalNonAssocSemiring FreeMagma FreeMagma.instMul MonoidAlgebra.distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike_1 Equiv EquivLike.toFunLike Equiv.instEquivLike lift of	—	Equiv.left_inv

(root)

Definitions

Name	Category	Theorems
FreeNonUnitalNonAssocAlgebra 📖	CompOp	15 math math: FreeNonUnitalNonAssocAlgebra.of_comp_lift, FreeLieAlgebra.Rel.addLeft, FreeNonUnitalNonAssocAlgebra.lift_unique, FreeLieAlgebra.liftAux_map_smul, FreeLieAlgebra.liftAux_map_add, FreeNonUnitalNonAssocAlgebra.lift_symm_apply, FreeLieAlgebra.liftAux_map_mul, FreeLieAlgebra.liftAux_spec, FreeLieAlgebra.Rel.neg, FreeLieAlgebra.Rel.subRight, FreeLieAlgebra.Rel.subLeft, FreeLieAlgebra.Rel.smulOfTower, FreeNonUnitalNonAssocAlgebra.lift_of_apply, FreeNonUnitalNonAssocAlgebra.hom_ext_iff, FreeNonUnitalNonAssocAlgebra.lift_comp_of

---

← Back to Index