MonoidAlgebra

📁 Source: Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

Statistics

Metric	Count
Definitions instBialgebra, mapDomainBialgHom, instBialgebra, instBialgebra, mapDomainBialgHom	5
Theorems mapDomainBialgHom_apply, mapDomainBialgHom_comp, mapDomainBialgHom_id, mapDomainBialgHom_mapDomainBialgHom, comul_T, counit_T, mapDomainBialgHom_apply, mapDomainBialgHom_comp, mapDomainBialgHom_id, mapDomainBialgHom_mapDomainBialgHom	10
Total	15

AddMonoidAlgebra

Definitions

Name	Category	Theorems
instBialgebra 📖	CompOp	—
mapDomainBialgHom 📖	CompOp	4 math math: mapDomainBialgHom_id, mapDomainBialgHom_mapDomainBialgHom, mapDomainBialgHom_apply, mapDomainBialgHom_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapDomainBialgHom_apply 📖	mathematical	—	DFunLike.coe BialgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCoalgebra Semiring.toModule Bialgebra.toCoalgebra CommSemiring.toBialgebra BialgHom.funLike mapDomainBialgHom mapDomain AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	—	—
mapDomainBialgHom_comp 📖	mathematical	—	mapDomainBialgHom AddMonoidHom.comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass BialgHom.comp AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCoalgebra Semiring.toModule Bialgebra.toCoalgebra CommSemiring.toBialgebra	—	BialgHom.ext ext Finsupp.mapDomain_comp
mapDomainBialgHom_id 📖	mathematical	—	mapDomainBialgHom AddMonoidHom.id AddZeroClass.toAddZero AddMonoid.toAddZeroClass BialgHom.id AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCoalgebra Semiring.toModule Bialgebra.toCoalgebra CommSemiring.toBialgebra	—	BialgHom.ext ext Finsupp.mapDomain_id
mapDomainBialgHom_mapDomainBialgHom 📖	mathematical	—	DFunLike.coe BialgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCoalgebra Semiring.toModule Bialgebra.toCoalgebra CommSemiring.toBialgebra BialgHom.funLike mapDomainBialgHom AddMonoidHom.comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	ext mapDomainBialgHom_comp

LaurentPolynomial

Definitions

Name	Category	Theorems
instBialgebra 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_T 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial TensorProduct AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module Algebra.toModule Bialgebra.toAlgebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct instCoalgebra Bialgebra.toCoalgebra T TensorProduct.tmul	—	AddMonoidAlgebra.comul_single Bialgebra.comul_one
counit_T 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial AddMonoidAlgebra.addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.module Algebra.toModule Bialgebra.toAlgebra Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct instCoalgebra Bialgebra.toCoalgebra T AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	AddMonoidAlgebra.counit_single Bialgebra.counit_one

MonoidAlgebra

Definitions

Name	Category	Theorems
instBialgebra 📖	CompOp	—
mapDomainBialgHom 📖	CompOp	4 math math: mapDomainBialgHom_comp, mapDomainBialgHom_mapDomainBialgHom, mapDomainBialgHom_apply, mapDomainBialgHom_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapDomainBialgHom_apply 📖	mathematical	—	DFunLike.coe BialgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCoalgebra Semiring.toModule Bialgebra.toCoalgebra CommSemiring.toBialgebra BialgHom.funLike mapDomainBialgHom mapDomain MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	—
mapDomainBialgHom_comp 📖	mathematical	—	mapDomainBialgHom MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass BialgHom.comp MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCoalgebra Semiring.toModule Bialgebra.toCoalgebra CommSemiring.toBialgebra	—	BialgHom.ext ext Finsupp.mapDomain_comp
mapDomainBialgHom_id 📖	mathematical	—	mapDomainBialgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass BialgHom.id MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCoalgebra Semiring.toModule Bialgebra.toCoalgebra CommSemiring.toBialgebra	—	BialgHom.ext ext Finsupp.mapDomain_id
mapDomainBialgHom_mapDomainBialgHom 📖	mathematical	—	DFunLike.coe BialgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCoalgebra Semiring.toModule Bialgebra.toCoalgebra CommSemiring.toBialgebra BialgHom.funLike mapDomainBialgHom MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass	—	ext mapDomainBialgHom_comp

---

← Back to Index