MonoidAlgebra

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

Statistics

Metric	Count
Definitions instCoalgebra, instCoalgebra, instCoalgebra	3
Theorems comul_single, counit_single, instIsCocomm, comul_C, comul_C_mul_T, comul_C_mul_T_self, counit_C, counit_C_mul_T, instIsCocomm, comul_single, counit_single, instIsCocomm	12
Total	15

AddMonoidAlgebra

Definitions

Name	Category	Theorems
instCoalgebra 📖	CompOp	7 math math: comul_single, mapDomainBialgHom_id, counit_single, mapDomainBialgHom_mapDomainBialgHom, mapDomainBialgHom_apply, mapDomainBialgHom_comp, instIsCocomm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddMonoidAlgebra TensorProduct addAddCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct instCoalgebra single NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct.map lsingle	—	Finsupp.comul_single
counit_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddMonoidAlgebra addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct instCoalgebra single	—	Finsupp.counit_single
instIsCocomm 📖	mathematical	—	Coalgebra.IsCocomm AddMonoidAlgebra addAddCommMonoid module CommSemiring.toSemiring instCoalgebra	—	Finsupp.instIsCocomm

LaurentPolynomial

Definitions

Name	Category	Theorems
instCoalgebra 📖	CompOp	8 math math: comul_T, comul_C, counit_C_mul_T, instIsCocomm, counit_T, counit_C, comul_C_mul_T, comul_C_mul_T_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_C 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial TensorProduct AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct instCoalgebra RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra TensorProduct.map AddMonoidAlgebra.lsingle	—	AddMonoidAlgebra.comul_single
comul_C_mul_T 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddMonoidAlgebra TensorProduct AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct instCoalgebra LaurentPolynomial AddMonoidAlgebra.instMul RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct.map AddMonoidAlgebra.lsingle	—	AddMonoidAlgebra.comul_single
comul_C_mul_T_self 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial TensorProduct AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct instCoalgebra CommSemiring.toCoalgebra AddMonoidAlgebra.instMul RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T TensorProduct.tmul	—	comul_C_mul_T single_eq_C_mul_T map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul
counit_C 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial AddMonoidAlgebra.addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct instCoalgebra RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C	—	AddMonoidAlgebra.counit_single
counit_C_mul_T 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial AddMonoidAlgebra.addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct instCoalgebra AddMonoidAlgebra.instMul RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T	—	AddMonoidAlgebra.counit_single
instIsCocomm 📖	mathematical	—	Coalgebra.IsCocomm LaurentPolynomial AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module CommSemiring.toSemiring instCoalgebra	—	AddMonoidAlgebra.instIsCocomm

MonoidAlgebra

Definitions

Name	Category	Theorems
instCoalgebra 📖	CompOp	7 math math: instIsCocomm, mapDomainBialgHom_comp, mapDomainBialgHom_mapDomainBialgHom, mapDomainBialgHom_apply, comul_single, counit_single, mapDomainBialgHom_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MonoidAlgebra TensorProduct addCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct instCoalgebra single NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct.map lsingle	—	Finsupp.comul_single
counit_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MonoidAlgebra addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct instCoalgebra single	—	Finsupp.counit_single
instIsCocomm 📖	mathematical	—	Coalgebra.IsCocomm MonoidAlgebra addCommMonoid module CommSemiring.toSemiring instCoalgebra	—	Finsupp.instIsCocomm

---

← Back to Index