Basic

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

Statistics

Metric	Count
Definitions IsCocomm, Repr, arbitrary, index, left, right, ι, termℛ, toCoalgebraStruct, CoalgebraStruct, comul, counit, toCoalgebra, instCoalgebra, instCoalgebraStruct, coalgebra, coalgebraStruct, instCoalgebra, instCoalgebraStruct, instCoalgebra, instCoalgebraStruct, instCoalgebra, instCoalgebraStruct, termδ, termε	25
Theorems comm_comp_comul, eq, coassoc, coassoc_apply, coassoc_symm, coassoc_symm_apply, comm_comp_comul, comm_comul, lTensor_counit_comp_comul, lTensor_counit_comul, lift_lsmul_comp_counit_comp_comul, rTensor_counit_comp_comul, rTensor_counit_comul, sum_counit_smul, sum_counit_tmul_eq, sum_counit_tmul_map_eq, sum_map_tmul_counit_eq, sum_map_tmul_tmul_eq, sum_tmul_counit_eq, sum_tmul_tmul_eq, comul_apply, counit_apply, instIsCocomm, comul_comp_lapply, comul_comp_lsingle, comul_single, counit_comp_lsingle, counit_single, instIsCocomm, coalgebraIsCocomm, comul_comp_lapply, comul_comp_lsingle, comul_single, counit_comp_lsingle, counit_single, instIsCocomm, comul_coe_dFinsupp, comul_coe_finsupp, comul_comp_dFinsuppCoeFnLinearMap, comul_comp_finsuppLcoeFun, comul_comp_proj, comul_comp_single, comul_single, counit_coe_dFinsupp, counit_coe_finsupp, counit_comp_dFinsuppCoeFnLinearMap, counit_comp_finsuppLcoeFun, counit_comp_single, counit_single, instIsCocomm, comul_apply, comul_comp_fst, comul_comp_inl, comul_comp_inr, comul_comp_snd, counit_apply, counit_comp_inl, counit_comp_inr, instIsCocomm	59
Total	84

Coalgebra

Definitions

Name	Category	Theorems
IsCocomm 📖	CompData	8 math math: MonoidAlgebra.instIsCocomm, Prod.instIsCocomm, Equiv.coalgebraIsCocomm, Finsupp.instIsCocomm, TensorProduct.instIsCocomm, CommSemiring.instIsCocomm, AddMonoidAlgebra.instIsCocomm, LaurentPolynomial.instIsCocomm
Repr 📖	CompData	—
termℛ 📖	CompOp	—
toCoalgebraStruct 📖	CompOp	234 math math: Pi.comul_eq_adjoint, CoalgHom.ext_of_ring_iff, Bialgebra.comulAlgHom_apply, Bialgebra.comul_natCast, Repr.induced_ι, lTensor_counit_comul, HopfAlgCat.of_comul, CategoryTheory.Iso.toCoalgEquiv_symm, IsGroupLikeElem.comul_eq_tmul_self, LaurentPolynomial.comul_T, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, BialgEquiv.toHopfAlgIso_refl, CoalgCat.MonoidalCategoryAux.tensorHom_toLinearMap, BialgEquiv.toBialgIso_refl, Bialgebra.TensorProduct.map_toAlgHom, AddMonoidAlgebra.comul_single, CoalgCat.of_comul, CategoryTheory.Iso.toHopfAlgEquiv_trans, sum_map_tmul_counit_eq, sum_tmul_counit_eq, Prod.counit_comp_inr, CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap, coassoc_symm_apply, BialgCat.of_counit, Bialgebra.counitBialgHom_apply, Bialgebra.counitAlgHom_apply, CoalgEquiv.toCoalgIso_refl, CommBialgCat.id_apply, Repr.induced_index, sum_counit_tmul_eq, AddMonoidAlgebra.mapDomainBialgHom_id, HopfAlgCat.of_counit, CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CategoryTheory.Iso.toCoalgEquiv_toCoalgHom, CommBialgCat.isoEquivBialgEquiv_apply, Pi.counit_eq_adjoint, HopfAlgCat.Hom.toBialgHom_injective, HopfAlgCat.forget_reflects_isos, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, CommBialgCat.ofHom_comp, MonoidAlgebra.mapDomainBialgHom_comp, CategoryTheory.Iso.toBialgEquiv_refl, Bialgebra.TensorProduct.map_toCoalgHom, HopfAlgebra.sum_mul_antipode_eq_smul, sum_map_tmul_tmul_eq, LinearMap.convOne_apply, AddMonoidAlgebra.counit_single, Pi.intrinsicStar_comul_commSemiring, BialgCat.forget_reflects_isos, comm_comul, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, isGroupLikeElem_iff, MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom, AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, TensorProduct.lid_tmul, BialgCat.Hom.toBialgHom_injective, subsingleton_to_ring, Bialgebra.toLinearMap_counitAlgHom, CommBialgCat.forget₂_commAlgCat_obj, HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso, Bialgebra.counitBialgHom_self, CommBialgCat.bialgEquivOfIso_apply, CategoryTheory.Iso.toBialgEquiv_trans, BialgCat.of_comul, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left, Bialgebra.counit_surjective, HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso, sum_counit_smul, Bialgebra.TensorProduct.assoc_tmul, InnerProductSpace.AlgebraOfCoalgebra.mul_def, HopfAlgCat.toBialgHom_comp, BialgCat.forget₂_coalgebra_obj, CoalgCat.MonoidalCategoryAux.tensorObj_comul, AddMonoidAlgebra.mapDomainBialgHom_apply, CoalgCat.comul_def, CoalgCat.MonoidalCategory.inducingFunctorData_μIso, CoalgCat.MonoidalCategory.inducingFunctorData_εIso, Bialgebra.comul_algebraMap, HopfAlgebra.sum_antipode_mul_eq_smul, MonoidAlgebra.mapDomainBialgHom_apply, sum_counit_tmul_map_eq, CommBialgCat.reflectsIsomorphisms_forget, BialgCat.forget₂_algebra_map, CommBialgCat.inv_hom_apply, BialgEquiv.toBialgIso_symm, CategoryTheory.Iso.toCoalgEquiv_refl, IsCocomm.comm_comp_comul, HopfAlgCat.forget₂_bialgebra_obj, Prod.comul_apply, BialgEquiv.toLinearMap_ofAlgEquiv, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, rTensor_counit_comp_comul, CoalgCat.forget_reflects_isos, CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap, TensorProduct.map_tmul, CommBialgCat.hom_inv_apply, CoalgEquiv.toCoalgIso_inv, BialgHomClass.counitAlgHom_comp, Bialgebra.TensorProduct.rid_toAlgEquiv, BialgHom.ofAlgHom_apply, CategoryTheory.Iso.toBialgEquiv_symm, Bialgebra.counit_natCast, counitCoalgHom_toLinearMap, BialgEquiv.toHopfAlgIso_symm, Bialgebra.comul_mul, HopfAlgebra.mul_antipode_rTensor_comul, CoalgCat.Hom.toCoalgHom_injective, CommBialgCat.isoEquivBialgEquiv_symm_apply, CategoryTheory.Iso.toHopfAlgEquiv_symm, CategoryTheory.Iso.toCoalgEquiv_trans, coassoc, HopfAlgebra.counit_comp_antipode, lift_lsmul_comp_counit_comp_comul, LinearMap.convOne_def, Bialgebra.counit_mul, Bialgebra.TensorProduct.map_tmul, CoalgCat.MonoidalCategoryAux.counit_tensorObj, CoalgCat.counit_def, LaurentPolynomial.comul_C, HopfAlgebra.mul_antipode_rTensor_comul_apply, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, Bialgebra.counitBialgHom_toCoalgHom, HopfAlgCat.toBialgHom_id, CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left, CoalgCat.forget₂_obj, sum_tmul_tmul_eq, HopfAlgebra.counit_antipode, LinearMap.nonUnitalAlgHom_comp_convMul_distrib, MonoidAlgebra.comul_single, CommBialgCat.comp_apply, BialgHomClass.map_comp_comulAlgHom, BialgCat.MonoidalCategory.inducingFunctorData_μIso, CommBialgCat.bialgEquivOfIso_symm_apply, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right, CoalgCat.forget₂_map, Bialgebra.TensorProduct.lid_toAlgEquiv, BialgCat.toBialgHom_id, TensorProduct.assoc_tmul, Prod.comul_comp_fst, LaurentPolynomial.counit_C_mul_T, CategoryTheory.Iso.toHopfAlgEquiv_refl, TensorProduct.lid_toLinearEquiv, HopfAlgCat.forget₂_bialgebra_map, Prod.comul_comp_snd, IsGroupLikeElem.counit_eq_one, Bialgebra.counit_algebraMap, rTensor_counit_comul, TensorProduct.assoc_symm_tmul, AddMonoidAlgebra.mapDomainBialgHom_comp, LinearMap.toSpanSingleton_convMul_toSpanSingleton, CommBialgCat.isoMk_hom, CoalgCat.MonoidalCategoryAux.comul_tensorObj, CommBialgCat.forget_obj, Bialgebra.comul_pow, counitCoalgHom_apply, BialgEquiv.toBialgIso_trans, Bialgebra.comul_one, CommBialgCat.ofHom_apply, Bialgebra.TensorProduct.assoc_toCoalgEquiv, LaurentPolynomial.counit_T, CoalgCat.toComon_map_hom, TensorProduct.rid_symm_apply, LaurentPolynomial.counit_C, LinearMap.convMul_comp_coalgHom_distrib, Bialgebra.TensorProduct.lid_toCoalgEquiv, coassoc_apply, TensorProduct.rid_toLinearEquiv, HopfAlgebra.mul_antipode_lTensor_comul_apply, BialgCat.forget₂_coalgebra_map, Bialgebra.TensorProduct.rid_symm_apply, Bialgebra.counit_one, BialgEquiv.toHopfAlgIso_trans, coassoc_symm, LaurentPolynomial.comul_C_mul_T, Prod.comul_comp_inl, lTensor_counit_comp_comul, TensorProduct.rid_tmul, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, Bialgebra.subsingleton_to_ring, BialgEquiv.toBialgIso_hom, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, BialgCat.toBialgHom_comp, Bialgebra.TensorProduct.rid_tmul, Bialgebra.TensorProduct.lid_tmul, HopfAlgebra.mul_antipode_lTensor_comul, CategoryTheory.Iso.toBialgEquiv_toBialgHom, CommBialgCat.isoMk_inv, TensorProduct.map_toLinearMap, CommBialgCat.forget_map, CommBialgCat.ofHom_id, Bialgebra.toLinearMap_comulAlgHom, CommBialgCat.forget₂_commAlgCat_map, Prod.counit_apply, Prod.comul_comp_inr, BialgHom.ext_of_ring_iff, CoalgEquiv.toCoalgIso_symm, BialgEquiv.toHopfAlgIso_hom, CommSemiring.counit_apply, CoalgCat.toCoalgHom_id, CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom, Bialgebra.TensorProduct.lid_symm_apply, Bialgebra.TensorProduct.rid_toCoalgEquiv, TensorProduct.assoc_toLinearEquiv, Bialgebra.counit_pow, Bialgebra.mul_compr₂_comul, BialgCat.forget₂_algebra_obj, CoalgCat.toCoalgHom_comp, CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap, CoalgCat.of_counit, CommBialgCat.hom_id, Repr.induced_right, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, Prod.counit_comp_inl, BialgEquiv.toHopfAlgIso_inv, MonoidAlgebra.counit_single, CommBialgCat.hom_comp, Bialgebra.mul_compr₂_counit, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, LaurentPolynomial.comul_C_mul_T_self, BialgCat.MonoidalCategory.inducingFunctorData_εIso, comm_comp_comul, Bialgebra.TensorProduct.assoc_symm_tmul, Bialgebra.TensorProduct.assoc_toAlgEquiv, TensorProduct.lid_symm_apply, MonoidAlgebra.mapDomainBialgHom_id, CoalgEquiv.toCoalgIso_trans, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, CoalgEquiv.toCoalgIso_hom, CommSemiring.comul_apply, Repr.induced_left, BialgEquiv.ofAlgEquiv_apply, BialgEquiv.toBialgIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coassoc 📖	mathematical	—	LinearMap.comp TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.assoc LinearMap.rTensor CoalgebraStruct.comul toCoalgebraStruct LinearMap.lTensor	—	—
coassoc_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv TensorProduct.assoc LinearMap LinearMap.instFunLike LinearMap.rTensor CoalgebraStruct.comul toCoalgebraStruct LinearMap.lTensor	—	LinearMap.congr_fun RingHomCompTriple.ids RingHomInvPair.ids coassoc
coassoc_symm 📖	mathematical	—	LinearMap.comp TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm TensorProduct.assoc LinearMap.lTensor CoalgebraStruct.comul toCoalgebraStruct LinearMap.rTensor	—	LinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids coassoc_symm_apply
coassoc_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm TensorProduct.assoc LinearMap LinearMap.instFunLike LinearMap.lTensor CoalgebraStruct.comul toCoalgebraStruct LinearMap.rTensor	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq coassoc_apply
comm_comp_comul 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.comm CoalgebraStruct.comul toCoalgebraStruct	—	IsCocomm.comm_comp_comul
comm_comul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv TensorProduct.comm LinearMap LinearMap.instFunLike CoalgebraStruct.comul toCoalgebraStruct	—	RingHomInvPair.ids RingHomCompTriple.ids comm_comp_comul
lTensor_counit_comp_comul 📖	mathematical	—	LinearMap.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id RingHomCompTriple.ids LinearMap.lTensor CoalgebraStruct.counit toCoalgebraStruct CoalgebraStruct.comul DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.smulCommClass_left smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.instFunLike LinearMap.flip AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
lTensor_counit_comul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor CoalgebraStruct.counit toCoalgebraStruct CoalgebraStruct.comul TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	LinearMap.congr_fun RingHomCompTriple.ids SMulCommClass.symm TensorProduct.smulCommClass_left smulCommClass_self lTensor_counit_comp_comul
lift_lsmul_comp_counit_comp_comul 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids TensorProduct.lift LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.lsmul CoalgebraStruct.counit toCoalgebraStruct CoalgebraStruct.comul LinearMap.id	—	RingHomCompTriple.ids TensorProduct.smulCommClass_left smulCommClass_self rTensor_counit_comp_comul LinearMap.ext LinearMap.compl₂_id TensorProduct.lift_comp_map LinearMap.comp_assoc LinearMap.rTensor.eq_1 one_smul
rTensor_counit_comp_comul 📖	mathematical	—	LinearMap.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id RingHomCompTriple.ids LinearMap.rTensor CoalgebraStruct.counit toCoalgebraStruct CoalgebraStruct.comul DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid LinearMap.instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
rTensor_counit_comul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor CoalgebraStruct.counit toCoalgebraStruct CoalgebraStruct.comul TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	LinearMap.congr_fun RingHomCompTriple.ids TensorProduct.smulCommClass_left smulCommClass_self rTensor_counit_comp_comul
sum_counit_smul 📖	mathematical	—	Finset.sum Repr.ι toCoalgebraStruct Repr.index SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Repr.left Repr.right	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr one_smul sum_counit_tmul_eq
sum_counit_tmul_eq 📖	mathematical	—	Finset.sum Repr.ι toCoalgebraStruct TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid Repr.index TensorProduct.tmul DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike CoalgebraStruct.counit Repr.left Repr.right AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomCompTriple.ids TensorProduct.smulCommClass_left smulCommClass_self Repr.eq map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr rTensor_counit_comp_comul
sum_counit_tmul_map_eq 📖	mathematical	—	Finset.sum Repr.ι toCoalgebraStruct TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid Repr.index TensorProduct.tmul DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike CoalgebraStruct.counit Repr.left Repr.right AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	sum_counit_tmul_eq map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr
sum_map_tmul_counit_eq 📖	mathematical	—	Finset.sum Repr.ι toCoalgebraStruct TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid Repr.index TensorProduct.tmul DFunLike.coe Repr.left LinearMap RingHom.id LinearMap.instFunLike CoalgebraStruct.counit Repr.right AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	sum_tmul_counit_eq map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr
sum_map_tmul_tmul_eq 📖	mathematical	—	Finset.sum Repr.ι toCoalgebraStruct TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule Repr.index Repr.right TensorProduct.tmul DFunLike.coe Repr.left	—	sum_tmul_tmul_eq map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr
sum_tmul_counit_eq 📖	mathematical	—	Finset.sum Repr.ι toCoalgebraStruct TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid Repr.index TensorProduct.tmul Repr.left DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike CoalgebraStruct.counit Repr.right AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomCompTriple.ids SMulCommClass.symm TensorProduct.smulCommClass_left smulCommClass_self Repr.eq map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr lTensor_counit_comp_comul
sum_tmul_tmul_eq 📖	mathematical	—	Finset.sum Repr.ι toCoalgebraStruct TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule Repr.index Repr.left TensorProduct.tmul Repr.right	—	Finset.sum_congr Repr.eq RingHomCompTriple.ids RingHomInvPair.ids map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass TensorProduct.sum_tmul SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass coassoc

Coalgebra.IsCocomm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm_comp_comul 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.comm CoalgebraStruct.comul Coalgebra.toCoalgebraStruct	—	—

Coalgebra.Repr

Definitions

Name	Category	Theorems
arbitrary 📖	CompOp	—
index 📖	CompOp	14 math math: Coalgebra.sum_map_tmul_counit_eq, Coalgebra.sum_tmul_counit_eq, induced_index, Coalgebra.sum_counit_tmul_eq, HopfAlgebra.sum_mul_antipode_eq_smul, Coalgebra.sum_map_tmul_tmul_eq, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, Coalgebra.sum_counit_smul, HopfAlgebra.sum_antipode_mul_eq_smul, Coalgebra.sum_counit_tmul_map_eq, convMul_apply, Coalgebra.sum_tmul_tmul_eq, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, eq
left 📖	CompOp	14 math math: Coalgebra.sum_map_tmul_counit_eq, Coalgebra.sum_tmul_counit_eq, Coalgebra.sum_counit_tmul_eq, HopfAlgebra.sum_mul_antipode_eq_smul, Coalgebra.sum_map_tmul_tmul_eq, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, Coalgebra.sum_counit_smul, HopfAlgebra.sum_antipode_mul_eq_smul, Coalgebra.sum_counit_tmul_map_eq, convMul_apply, Coalgebra.sum_tmul_tmul_eq, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, eq, induced_left
right 📖	CompOp	14 math math: Coalgebra.sum_map_tmul_counit_eq, Coalgebra.sum_tmul_counit_eq, Coalgebra.sum_counit_tmul_eq, HopfAlgebra.sum_mul_antipode_eq_smul, Coalgebra.sum_map_tmul_tmul_eq, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, Coalgebra.sum_counit_smul, HopfAlgebra.sum_antipode_mul_eq_smul, Coalgebra.sum_counit_tmul_map_eq, convMul_apply, Coalgebra.sum_tmul_tmul_eq, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, eq, induced_right
ι 📖	CompOp	16 math math: induced_ι, Coalgebra.sum_map_tmul_counit_eq, Coalgebra.sum_tmul_counit_eq, Coalgebra.sum_counit_tmul_eq, HopfAlgebra.sum_mul_antipode_eq_smul, Coalgebra.sum_map_tmul_tmul_eq, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, Coalgebra.sum_counit_smul, HopfAlgebra.sum_antipode_mul_eq_smul, Coalgebra.sum_counit_tmul_map_eq, convMul_apply, Coalgebra.sum_tmul_tmul_eq, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, eq, induced_right, induced_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	—	Finset.sum ι TensorProduct TensorProduct.addCommMonoid index TensorProduct.tmul left right DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul	—	—

CoalgebraStruct

Definitions

Name	Category	Theorems
comul 📖	CompOp	73 math math: Pi.comul_eq_adjoint, DFinsupp.comul_single, Bialgebra.comulAlgHom_apply, Bialgebra.comul_natCast, Coalgebra.lTensor_counit_comul, HopfAlgCat.of_comul, IsGroupLikeElem.comul_eq_tmul_self, LinearMap.convMul_def, LaurentPolynomial.comul_T, AddMonoidAlgebra.comul_single, Pi.comul_comp_dFinsuppCoeFnLinearMap, CoalgCat.of_comul, Coalgebra.coassoc_symm_apply, Pi.comul_comp_single, CoalgHom.map_comp_comul, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, Pi.intrinsicStar_comul_commSemiring, Coalgebra.comm_comul, isGroupLikeElem_iff, BialgCat.of_comul, Finsupp.comul_comp_lapply, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left, InnerProductSpace.AlgebraOfCoalgebra.mul_def, CoalgCat.MonoidalCategoryAux.tensorObj_comul, CoalgCat.comul_def, Bialgebra.comul_algebraMap, DFinsupp.comul_comp_lapply, Coalgebra.IsCocomm.comm_comp_comul, Prod.comul_apply, Coalgebra.rTensor_counit_comp_comul, CoalgHomClass.map_comp_comul, CoalgCat.ofComonObjCoalgebraStruct_comul, Bialgebra.comul_mul, HopfAlgebra.mul_antipode_rTensor_comul, Coalgebra.coassoc, DFinsupp.comul_comp_lsingle, Coalgebra.lift_lsmul_comp_counit_comp_comul, LaurentPolynomial.comul_C, Finsupp.comul_single, HopfAlgebra.mul_antipode_rTensor_comul_apply, MonoidAlgebra.comul_single, Pi.comul_coe_finsupp, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right, TensorProduct.comul_tmul, Prod.comul_comp_fst, TensorProduct.comul_def, Prod.comul_comp_snd, Pi.comul_comp_proj, Coalgebra.rTensor_counit_comul, CoalgCat.MonoidalCategoryAux.comul_tensorObj, Bialgebra.comul_pow, Bialgebra.comul_one, Pi.comul_single, Coalgebra.coassoc_apply, HopfAlgebra.mul_antipode_lTensor_comul_apply, MulOpposite.comul_def, Coalgebra.coassoc_symm, LaurentPolynomial.comul_C_mul_T, Prod.comul_comp_inl, Coalgebra.lTensor_counit_comp_comul, HopfAlgebra.mul_antipode_lTensor_comul, Pi.comul_coe_dFinsupp, Bialgebra.toLinearMap_comulAlgHom, LinearMap.convMul_apply, Prod.comul_comp_inr, Finsupp.comul_comp_lsingle, CoalgHomClass.map_comp_comul_apply, Coalgebra.Repr.eq, Bialgebra.mul_compr₂_comul, LaurentPolynomial.comul_C_mul_T_self, Coalgebra.comm_comp_comul, CommSemiring.comul_apply, Pi.comul_comp_finsuppLcoeFun
counit 📖	CompOp	71 math math: Coalgebra.lTensor_counit_comul, Pi.counit_coe_dFinsupp, Coalgebra.sum_map_tmul_counit_eq, Coalgebra.sum_tmul_counit_eq, Prod.counit_comp_inr, BialgCat.of_counit, Bialgebra.counitBialgHom_apply, Bialgebra.counitAlgHom_apply, Coalgebra.sum_counit_tmul_eq, Pi.counit_comp_finsuppLcoeFun, HopfAlgCat.of_counit, CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right, Pi.counit_eq_adjoint, Pi.counit_comp_dFinsuppCoeFnLinearMap, HopfAlgebra.sum_mul_antipode_eq_smul, LinearMap.convOne_apply, AddMonoidAlgebra.counit_single, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, isGroupLikeElem_iff, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, Bialgebra.toLinearMap_counitAlgHom, Bialgebra.counit_surjective, Coalgebra.sum_counit_smul, CoalgHomClass.counit_comp_apply, CoalgHom.counit_comp, DFinsupp.counit_comp_lsingle, Finsupp.counit_comp_lsingle, TensorProduct.counit_tmul, HopfAlgebra.sum_antipode_mul_eq_smul, Coalgebra.sum_counit_tmul_map_eq, MulOpposite.counit_def, Coalgebra.rTensor_counit_comp_comul, Bialgebra.counit_natCast, Coalgebra.counitCoalgHom_toLinearMap, HopfAlgebra.mul_antipode_rTensor_comul, Finsupp.counit_single, HopfAlgebra.counit_comp_antipode, Coalgebra.lift_lsmul_comp_counit_comp_comul, LinearMap.convOne_def, Bialgebra.counit_mul, CoalgCat.MonoidalCategoryAux.counit_tensorObj, CoalgCat.counit_def, HopfAlgebra.mul_antipode_rTensor_comul_apply, Pi.counit_coe_finsupp, CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left, TensorProduct.counit_def, HopfAlgebra.counit_antipode, CoalgHomClass.counit_comp, LaurentPolynomial.counit_C_mul_T, IsGroupLikeElem.counit_eq_one, Bialgebra.counit_algebraMap, Coalgebra.rTensor_counit_comul, Coalgebra.counitCoalgHom_apply, LaurentPolynomial.counit_T, LaurentPolynomial.counit_C, DFinsupp.counit_single, HopfAlgebra.mul_antipode_lTensor_comul_apply, Bialgebra.counit_one, Coalgebra.lTensor_counit_comp_comul, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, HopfAlgebra.mul_antipode_lTensor_comul, CoalgCat.ofComonObjCoalgebraStruct_counit, Prod.counit_apply, CommSemiring.counit_apply, Pi.counit_comp_single, Bialgebra.counit_pow, CoalgCat.of_counit, Prod.counit_comp_inl, MonoidAlgebra.counit_single, Bialgebra.mul_compr₂_counit, Pi.counit_single

CommSemiring

Definitions

Name	Category	Theorems
toCoalgebra 📖	CompOp	23 math math: Pi.comul_eq_adjoint, CoalgHom.ext_of_ring_iff, Pi.counit_eq_adjoint, Pi.intrinsicStar_comul_commSemiring, Coalgebra.TensorProduct.lid_tmul, Coalgebra.subsingleton_to_ring, CoalgCat.tensorUnit_instCoalgebra, Coalgebra.counitCoalgHom_toLinearMap, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, isGroupLikeElem_self, Coalgebra.TensorProduct.lid_toLinearEquiv, instIsCocomm, LinearMap.toSpanSingleton_convMul_toSpanSingleton, Coalgebra.counitCoalgHom_apply, Coalgebra.TensorProduct.rid_symm_apply, Coalgebra.TensorProduct.rid_toLinearEquiv, CoalgCat.rightUnitor_def, Coalgebra.TensorProduct.rid_tmul, counit_apply, CoalgCat.leftUnitor_def, LaurentPolynomial.comul_C_mul_T_self, Coalgebra.TensorProduct.lid_symm_apply, comul_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_apply 📖	mathematical	—	DFunLike.coe LinearMap toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
counit_apply 📖	mathematical	—	DFunLike.coe LinearMap toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra	—	—
instIsCocomm 📖	mathematical	—	Coalgebra.IsCocomm NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toSemiring Semiring.toModule toCoalgebra	—	LinearMap.ext_ring RingHomCompTriple.ids RingHomInvPair.ids

DFinsupp

Definitions

Name	Category	Theorems
instCoalgebra 📖	CompOp	1 math math: instIsCocomm
instCoalgebraStruct 📖	CompOp	9 math math: comul_single, Pi.comul_comp_dFinsuppCoeFnLinearMap, Pi.counit_coe_dFinsupp, Pi.counit_comp_dFinsuppCoeFnLinearMap, counit_comp_lsingle, comul_comp_lapply, comul_comp_lsingle, counit_single, Pi.comul_coe_dFinsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_comp_lapply 📖	mathematical	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct CommSemiring.toSemiring addCommMonoid TensorProduct.addCommMonoid module TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul lapply TensorProduct.map instCoalgebraStruct	—	lhom_ext' RingHomCompTriple.ids LinearMap.ext eq_or_ne single_apply comul_single TensorProduct.map_map lapply_comp_lsingle_same TensorProduct.map_id lapply_comp_lsingle_of_ne TensorProduct.map_zero_right map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
comul_comp_lsingle 📖	mathematical	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct addCommMonoid module CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul instCoalgebraStruct lsingle TensorProduct.map	—	LinearMap.ext RingHomCompTriple.ids comul_single
comul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct addCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul instCoalgebraStruct single TensorProduct.map lsingle	—	lsum_single
counit_comp_lsingle 📖	mathematical	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid CommSemiring.toSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring module Semiring.toModule RingHom.id RingHomCompTriple.ids CoalgebraStruct.counit instCoalgebraStruct lsingle	—	LinearMap.ext RingHomCompTriple.ids counit_single
counit_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit instCoalgebraStruct single	—	lsum_single
instIsCocomm 📖	mathematical	Coalgebra.IsCocomm	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module CommSemiring.toSemiring instCoalgebra	—	lhom_ext' RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext comul_single Coalgebra.comm_comul

Equiv

Definitions

Name	Category	Theorems
coalgebra 📖	CompOp	1 math math: coalgebraIsCocomm
coalgebraStruct 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coalgebraIsCocomm 📖	mathematical	—	Coalgebra.IsCocomm addCommMonoid module CommSemiring.toSemiring coalgebra	—	LinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids Coalgebra.comm_comul

Finsupp

Definitions

Name	Category	Theorems
instCoalgebra 📖	CompOp	1 math math: instIsCocomm
instCoalgebraStruct 📖	CompOp	9 math math: Pi.counit_comp_finsuppLcoeFun, comul_comp_lapply, counit_comp_lsingle, counit_single, comul_single, Pi.counit_coe_finsupp, Pi.comul_coe_finsupp, comul_comp_lsingle, Pi.comul_comp_finsuppLcoeFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_comp_lapply 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct CommSemiring.toSemiring instAddCommMonoid TensorProduct.addCommMonoid module TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul lapply TensorProduct.map instCoalgebraStruct	—	lhom_ext' RingHomCompTriple.ids LinearMap.ext eq_or_ne comul_single TensorProduct.map_map single_eq_same lapply_comp_lsingle_same TensorProduct.map_id single_eq_of_ne map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass lapply_comp_lsingle_of_ne TensorProduct.map_zero_right
comul_comp_lsingle 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct instAddCommMonoid module CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul instCoalgebraStruct lsingle TensorProduct.map	—	LinearMap.ext RingHomCompTriple.ids comul_single
comul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct instAddCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul instCoalgebraStruct single TensorProduct.map lsingle	—	lsum_single
counit_comp_lsingle 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid CommSemiring.toSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring module Semiring.toModule RingHom.id RingHomCompTriple.ids CoalgebraStruct.counit instCoalgebraStruct lsingle	—	LinearMap.ext RingHomCompTriple.ids counit_single
counit_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit instCoalgebraStruct single	—	lsum_single
instIsCocomm 📖	mathematical	—	Coalgebra.IsCocomm Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module CommSemiring.toSemiring instCoalgebra	—	lhom_ext' RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext comul_single Coalgebra.comm_comul

Pi

Definitions

Name	Category	Theorems
instCoalgebra 📖	CompOp	1 math math: instIsCocomm
instCoalgebraStruct 📖	CompOp	17 math math: comul_eq_adjoint, comul_comp_dFinsuppCoeFnLinearMap, counit_coe_dFinsupp, comul_comp_single, counit_comp_finsuppLcoeFun, counit_eq_adjoint, counit_comp_dFinsuppCoeFnLinearMap, intrinsicStar_comul_commSemiring, intrinsicStar_comul, counit_coe_finsupp, comul_coe_finsupp, comul_comp_proj, comul_single, comul_coe_dFinsupp, counit_comp_single, counit_single, comul_comp_finsuppLcoeFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_coe_dFinsupp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul instCoalgebraStruct DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike DFinsupp.addCommMonoid DFinsupp.module TensorProduct.map DFinsupp.coeFnLinearMap DFinsupp.instCoalgebraStruct	—	RingHomCompTriple.ids comul_comp_dFinsuppCoeFnLinearMap
comul_coe_finsupp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul instCoalgebraStruct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Function.module TensorProduct.map Finsupp.lcoeFun Finsupp.instCoalgebraStruct	—	RingHomCompTriple.ids comul_comp_finsuppLcoeFun
comul_comp_dFinsuppCoeFnLinearMap 📖	mathematical	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct addCommMonoid module CommSemiring.toSemiring DFinsupp.addCommMonoid TensorProduct.addCommMonoid DFinsupp.module TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul instCoalgebraStruct DFinsupp.coeFnLinearMap TensorProduct.map DFinsupp.instCoalgebraStruct	—	LinearMap.ext RingHomCompTriple.ids DFinsupp.sum_single DFinsupp.sum_eq_sum_fintype DFinsupp.single_zero Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass comul_single DFinsupp.comul_single TensorProduct.map_map
comul_comp_finsuppLcoeFun 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct addCommMonoid module CommSemiring.toSemiring Finsupp.instAddCommMonoid TensorProduct.addCommMonoid Finsupp.module TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul instCoalgebraStruct Finsupp.lcoeFun Function.module TensorProduct.map Finsupp.instCoalgebraStruct	—	LinearMap.ext RingHomCompTriple.ids Finsupp.univ_sum_single map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr Finsupp.single_eq_pi_single comul_single Finsupp.comul_single TensorProduct.map_map Finsupp.lcoeFun_comp_lsingle
comul_comp_proj 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring addCommMonoid TensorProduct.addCommMonoid module TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul LinearMap.proj TensorProduct.map instCoalgebraStruct	—	LinearMap.pi_ext' Finite.of_fintype RingHomCompTriple.ids LinearMap.ext eq_or_ne comul_single TensorProduct.map_map LinearMap.proj_comp_single single_eq_same Function.update_self TensorProduct.map_id single_eq_of_ne map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Function.update_of_ne TensorProduct.map_zero_right
comul_comp_single 📖	mathematical	—	LinearMap.comp TensorProduct addCommMonoid module CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul instCoalgebraStruct LinearMap.single TensorProduct.map	—	LinearMap.ext RingHomCompTriple.ids comul_single
comul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul instCoalgebraStruct single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct.map LinearMap.single	—	LinearMap.lsum_piSingle
counit_coe_dFinsupp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit instCoalgebraStruct DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike DFinsupp.addCommMonoid DFinsupp.module DFinsupp.instCoalgebraStruct	—	RingHomCompTriple.ids counit_comp_dFinsuppCoeFnLinearMap
counit_coe_finsupp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit instCoalgebraStruct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Finsupp.instCoalgebraStruct	—	RingHomCompTriple.ids counit_comp_finsuppLcoeFun
counit_comp_dFinsuppCoeFnLinearMap 📖	mathematical	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid CommSemiring.toSemiring DFinsupp.addCommMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFinsupp.module module Semiring.toModule RingHom.id RingHomCompTriple.ids CoalgebraStruct.counit instCoalgebraStruct DFinsupp.coeFnLinearMap DFinsupp.instCoalgebraStruct	—	LinearMap.ext RingHomCompTriple.ids DFinsupp.sum_single DFinsupp.sum_eq_sum_fintype DFinsupp.single_zero Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass counit_single DFinsupp.counit_single
counit_comp_finsuppLcoeFun 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid CommSemiring.toSemiring Finsupp.instAddCommMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.module module Semiring.toModule RingHom.id RingHomCompTriple.ids CoalgebraStruct.counit instCoalgebraStruct Finsupp.lcoeFun Finsupp.instCoalgebraStruct	—	LinearMap.ext RingHomCompTriple.ids Finsupp.univ_sum_single map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr Finsupp.single_eq_pi_single counit_single Finsupp.counit_single
counit_comp_single 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring module Semiring.toModule RingHom.id RingHomCompTriple.ids CoalgebraStruct.counit instCoalgebraStruct LinearMap.single	—	LinearMap.ext RingHomCompTriple.ids counit_single
counit_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit instCoalgebraStruct single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LinearMap.lsum_piSingle
instIsCocomm 📖	mathematical	Coalgebra.IsCocomm	addCommMonoid module CommSemiring.toSemiring instCoalgebra	—	LinearMap.pi_ext' Finite.of_fintype RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext comul_single Coalgebra.comm_comul

Prod

Definitions

Name	Category	Theorems
instCoalgebra 📖	CompOp	1 math math: instIsCocomm
instCoalgebraStruct 📖	CompOp	8 math math: counit_comp_inr, comul_apply, comul_comp_fst, comul_comp_snd, comul_comp_inl, counit_apply, comul_comp_inr, counit_comp_inl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct instAddCommMonoid instModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul instCoalgebraStruct TensorProduct.add TensorProduct.map LinearMap.inl Coalgebra.toCoalgebraStruct LinearMap.inr	—	—
comul_comp_fst 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring instAddCommMonoid TensorProduct.addCommMonoid instModule TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul Coalgebra.toCoalgebraStruct LinearMap.fst TensorProduct.map instCoalgebraStruct	—	LinearMap.prod_ext RingHomCompTriple.ids LinearMap.comp_assoc LinearMap.fst_comp_inl LinearMap.comp_id comul_comp_inl TensorProduct.map_comp TensorProduct.map_id RingHomCompTriple.right_ids LinearMap.id_comp LinearMap.fst_comp_inr LinearMap.comp_zero comul_comp_inr TensorProduct.map_zero_left LinearMap.zero_comp
comul_comp_inl 📖	mathematical	—	LinearMap.comp TensorProduct instAddCommMonoid instModule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul instCoalgebraStruct LinearMap.inl TensorProduct.map Coalgebra.toCoalgebraStruct	—	LinearMap.ext RingHomCompTriple.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass add_zero
comul_comp_inr 📖	mathematical	—	LinearMap.comp TensorProduct instAddCommMonoid instModule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul instCoalgebraStruct LinearMap.inr TensorProduct.map Coalgebra.toCoalgebraStruct	—	LinearMap.ext RingHomCompTriple.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass zero_add
comul_comp_snd 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring instAddCommMonoid TensorProduct.addCommMonoid instModule TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CoalgebraStruct.comul Coalgebra.toCoalgebraStruct LinearMap.snd TensorProduct.map instCoalgebraStruct	—	LinearMap.prod_ext RingHomCompTriple.ids LinearMap.comp_assoc LinearMap.snd_comp_inl LinearMap.comp_zero comul_comp_inl TensorProduct.map_comp TensorProduct.map_zero_left LinearMap.zero_comp LinearMap.snd_comp_inr LinearMap.comp_id comul_comp_inr TensorProduct.map_id RingHomCompTriple.right_ids LinearMap.id_comp
counit_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit instCoalgebraStruct Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Coalgebra.toCoalgebraStruct	—	—
counit_comp_inl 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instModule Semiring.toModule RingHom.id RingHomCompTriple.ids CoalgebraStruct.counit instCoalgebraStruct LinearMap.inl Coalgebra.toCoalgebraStruct	—	LinearMap.ext RingHomCompTriple.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass add_zero
counit_comp_inr 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instModule Semiring.toModule RingHom.id RingHomCompTriple.ids CoalgebraStruct.counit instCoalgebraStruct LinearMap.inr Coalgebra.toCoalgebraStruct	—	LinearMap.ext RingHomCompTriple.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass zero_add
instIsCocomm 📖	mathematical	—	Coalgebra.IsCocomm instAddCommMonoid instModule CommSemiring.toSemiring instCoalgebra	—	LinearMap.prod_ext RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass add_zero Coalgebra.comm_comul zero_add

RingTheory.LinearMap

Definitions

Name	Category	Theorems
termδ 📖	CompOp	—
termε 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
CoalgebraStruct 📖	CompData	—

---

← Back to Index