Basic

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

Statistics

Metric	Count
Definitions Bialgebra, comulAlgHom, counitAlgHom, mk', ofAlgHom, toAlgebra, toCoalgebra, toBialgebra	8
Theorems algebraMap_injective, comulAlgHom_apply, comul_algebraMap, comul_mul, comul_natCast, comul_one, comul_pow, counitAlgHom_apply, counitAlgHom_self, counit_algebraMap, counit_mul, counit_natCast, counit_one, counit_pow, counit_surjective, mul_compr₂_comul, mul_compr₂_counit, nontrivial, toLinearMap_comulAlgHom, toLinearMap_counitAlgHom	20
Total	28

Bialgebra

Definitions

Name	Category	Theorems
comulAlgHom 📖	CompOp	6 math math: comulAlgHom_apply, TensorProduct.comul_eq_algHom_toLinearMap, TensorProduct.comulAlgHom_def, CommAlgCat.mul_op_of_unop_hom, BialgHomClass.map_comp_comulAlgHom, toLinearMap_comulAlgHom
counitAlgHom 📖	CompOp	7 math math: TensorProduct.counitAlgHom_def, counitAlgHom_apply, TensorProduct.counit_eq_algHom_toLinearMap, toLinearMap_counitAlgHom, counitAlgHom_self, BialgHomClass.counitAlgHom_comp, CommAlgCat.one_op_of_unop_hom
mk' 📖	CompOp	—
ofAlgHom 📖	CompOp	—
toAlgebra 📖	CompOp	160 math math: comulAlgHom_apply, comul_natCast, HopfAlgCat.of_comul, BialgCat.rightUnitor_def, HopfAlgCat.rightUnitor_def, LaurentPolynomial.comul_T, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, BialgEquiv.toHopfAlgIso_refl, BialgEquiv.toBialgIso_refl, TensorProduct.map_toAlgHom, CategoryTheory.Iso.toHopfAlgEquiv_trans, MonoidAlgebra.antipode_single, HopfAlgCat.tensorObj_instRing, TensorProduct.counitAlgHom_def, BialgCat.of_counit, counitBialgHom_apply, counitAlgHom_apply, BialgCat.associator_def, CommBialgCat.id_apply, BialgCat.whiskerLeft_def, HopfAlgCat.whiskerLeft_def, HopfAlgCat.of_counit, HopfAlgCat.tensorObj_instHopfAlgebra, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CommBialgCat.isoEquivBialgEquiv_apply, HopfAlgCat.Hom.toBialgHom_injective, HopfAlgCat.forget_reflects_isos, TensorProduct.comul_eq_algHom_toLinearMap, CommBialgCat.ofHom_comp, CategoryTheory.Iso.toBialgEquiv_refl, TensorProduct.map_toCoalgHom, HopfAlgebra.sum_mul_antipode_eq_smul, BialgCat.forget_reflects_isos, LaurentPolynomial.antipode_T, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, TensorProduct.counit_eq_algHom_toLinearMap, BialgCat.Hom.toBialgHom_injective, algebraMap_injective, toLinearMap_counitAlgHom, CommBialgCat.forget₂_commAlgCat_obj, TensorProduct.comulAlgHom_def, HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso, CommBialgCat.bialgEquivOfIso_apply, CategoryTheory.Iso.toBialgEquiv_trans, BialgCat.of_comul, HopfAlgCat.whiskerRight_def, counit_surjective, HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, CommAlgCat.mul_op_of_unop_hom, TensorProduct.assoc_tmul, HopfAlgCat.toBialgHom_comp, BialgCat.forget₂_coalgebra_obj, GroupLike.valMonoidHom_apply, HopfAlgCat.associator_def, GroupLike.val_one, comul_algebraMap, HopfAlgebra.sum_antipode_mul_eq_smul, BialgCat.tensorHom_def, CommBialgCat.reflectsIsomorphisms_forget, BialgCat.forget₂_algebra_map, CommBialgCat.inv_hom_apply, BialgEquiv.toBialgIso_symm, HopfAlgCat.forget₂_bialgebra_obj, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, CommBialgCat.hom_inv_apply, BialgHomClass.counitAlgHom_comp, TensorProduct.rid_toAlgEquiv, CategoryTheory.Iso.toBialgEquiv_symm, counit_natCast, BialgEquiv.toHopfAlgIso_symm, comul_mul, HopfAlgebra.mul_antipode_rTensor_comul, GroupLike.val_mul, CommBialgCat.isoEquivBialgEquiv_symm_apply, CategoryTheory.Iso.toHopfAlgEquiv_symm, BialgCat.whiskerRight_def, HopfAlgebra.counit_comp_antipode, counit_mul, TensorProduct.map_tmul, isGroupLikeElem_unitsInv, HopfAlgebra.mul_antipode_rTensor_comul_apply, TensorProduct.coalgebra_rid_eq_algebra_rid_apply, GroupLike.val_toUnits_apply, counitBialgHom_toCoalgHom, HopfAlgCat.toBialgHom_id, BialgCat.tensorObj_def, CommAlgCat.one_op_of_unop_hom, HopfAlgCat.tensorHom_def, GroupLike.val_inv, HopfAlgebra.counit_antipode, CommBialgCat.comp_apply, CommSemiring.antipode_eq_id, BialgHomClass.map_comp_comulAlgHom, BialgCat.MonoidalCategory.inducingFunctorData_μIso, CommBialgCat.bialgEquivOfIso_symm_apply, TensorProduct.lid_toAlgEquiv, BialgCat.toBialgHom_id, CategoryTheory.Iso.toHopfAlgEquiv_refl, HopfAlgCat.forget₂_bialgebra_map, counit_algebraMap, LaurentPolynomial.antipode_C, CommBialgCat.isoMk_hom, CommBialgCat.forget_obj, GroupLike.val_inv_toUnits_apply, comul_pow, BialgEquiv.toBialgIso_trans, comul_one, CommBialgCat.ofHom_apply, TensorProduct.assoc_toCoalgEquiv, LaurentPolynomial.counit_T, TensorProduct.lid_toCoalgEquiv, HopfAlgebra.mul_antipode_lTensor_comul_apply, BialgCat.forget₂_coalgebra_map, TensorProduct.rid_symm_apply, counit_one, BialgEquiv.toHopfAlgIso_trans, HopfAlgCat.tensorObj_carrier, HopfAlgCat.leftUnitor_def, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, subsingleton_to_ring, BialgEquiv.toBialgIso_hom, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, BialgCat.toBialgHom_comp, TensorProduct.rid_tmul, TensorProduct.lid_tmul, HopfAlgebra.mul_antipode_lTensor_comul, CategoryTheory.Iso.toBialgEquiv_toBialgHom, GroupLike.val_pow, CommBialgCat.isoMk_inv, CommBialgCat.forget_map, CommBialgCat.ofHom_id, AddMonoidAlgebra.antipode_single, TensorProduct.antipode_def, toLinearMap_comulAlgHom, CommBialgCat.forget₂_commAlgCat_map, BialgEquiv.toHopfAlgIso_hom, IsGroupLikeElem.one, CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom, BialgCat.leftUnitor_def, TensorProduct.lid_symm_apply, TensorProduct.rid_toCoalgEquiv, counit_pow, mul_compr₂_comul, BialgCat.forget₂_algebra_obj, CommBialgCat.hom_id, instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, BialgEquiv.toHopfAlgIso_inv, CommBialgCat.hom_comp, mul_compr₂_counit, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, BialgCat.MonoidalCategory.inducingFunctorData_εIso, TensorProduct.assoc_symm_tmul, TensorProduct.assoc_toAlgEquiv, isGroupLikeElem_iff_of_mul_eq_one, HopfAlgebra.antipode_one, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, LaurentPolynomial.antipode_C_mul_T, BialgEquiv.toBialgIso_inv
toCoalgebra 📖	CompOp	142 math math: comulAlgHom_apply, comul_natCast, HopfAlgCat.of_comul, LaurentPolynomial.comul_T, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, BialgEquiv.toHopfAlgIso_refl, BialgEquiv.toBialgIso_refl, TensorProduct.map_toAlgHom, CategoryTheory.Iso.toHopfAlgEquiv_trans, BialgCat.of_counit, counitBialgHom_apply, counitAlgHom_apply, CommBialgCat.id_apply, AddMonoidAlgebra.mapDomainBialgHom_id, HopfAlgCat.of_counit, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CommBialgCat.isoEquivBialgEquiv_apply, HopfAlgCat.Hom.toBialgHom_injective, HopfAlgCat.forget_reflects_isos, TensorProduct.comul_eq_algHom_toLinearMap, CommBialgCat.ofHom_comp, MonoidAlgebra.mapDomainBialgHom_comp, CategoryTheory.Iso.toBialgEquiv_refl, TensorProduct.map_toCoalgHom, HopfAlgebra.sum_mul_antipode_eq_smul, BialgCat.forget_reflects_isos, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom, AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom, TensorProduct.counit_eq_algHom_toLinearMap, BialgCat.Hom.toBialgHom_injective, toLinearMap_counitAlgHom, CommBialgCat.forget₂_commAlgCat_obj, HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso, counitBialgHom_self, CommBialgCat.bialgEquivOfIso_apply, CategoryTheory.Iso.toBialgEquiv_trans, BialgCat.of_comul, counit_surjective, HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso, TensorProduct.assoc_tmul, HopfAlgCat.toBialgHom_comp, BialgCat.forget₂_coalgebra_obj, GroupLike.valMonoidHom_apply, AddMonoidAlgebra.mapDomainBialgHom_apply, GroupLike.val_one, comul_algebraMap, HopfAlgebra.sum_antipode_mul_eq_smul, MonoidAlgebra.mapDomainBialgHom_apply, CommBialgCat.reflectsIsomorphisms_forget, BialgCat.forget₂_algebra_map, CommBialgCat.inv_hom_apply, BialgEquiv.toBialgIso_symm, HopfAlgCat.forget₂_bialgebra_obj, BialgEquiv.toLinearMap_ofAlgEquiv, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, CommBialgCat.hom_inv_apply, BialgHomClass.counitAlgHom_comp, TensorProduct.rid_toAlgEquiv, BialgHom.ofAlgHom_apply, CategoryTheory.Iso.toBialgEquiv_symm, counit_natCast, BialgEquiv.toHopfAlgIso_symm, comul_mul, HopfAlgebra.mul_antipode_rTensor_comul, GroupLike.val_mul, CommBialgCat.isoEquivBialgEquiv_symm_apply, CategoryTheory.Iso.toHopfAlgEquiv_symm, HopfAlgebra.counit_comp_antipode, counit_mul, TensorProduct.map_tmul, isGroupLikeElem_unitsInv, HopfAlgebra.mul_antipode_rTensor_comul_apply, TensorProduct.coalgebra_rid_eq_algebra_rid_apply, GroupLike.val_toUnits_apply, counitBialgHom_toCoalgHom, HopfAlgCat.toBialgHom_id, GroupLike.val_inv, HopfAlgebra.counit_antipode, CommBialgCat.comp_apply, BialgHomClass.map_comp_comulAlgHom, BialgCat.MonoidalCategory.inducingFunctorData_μIso, CommBialgCat.bialgEquivOfIso_symm_apply, TensorProduct.lid_toAlgEquiv, BialgCat.toBialgHom_id, CategoryTheory.Iso.toHopfAlgEquiv_refl, HopfAlgCat.forget₂_bialgebra_map, counit_algebraMap, AddMonoidAlgebra.mapDomainBialgHom_comp, CommBialgCat.isoMk_hom, CommBialgCat.forget_obj, GroupLike.val_inv_toUnits_apply, comul_pow, BialgEquiv.toBialgIso_trans, comul_one, CommBialgCat.ofHom_apply, TensorProduct.assoc_toCoalgEquiv, LaurentPolynomial.counit_T, TensorProduct.lid_toCoalgEquiv, HopfAlgebra.mul_antipode_lTensor_comul_apply, BialgCat.forget₂_coalgebra_map, TensorProduct.rid_symm_apply, counit_one, BialgEquiv.toHopfAlgIso_trans, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, subsingleton_to_ring, BialgEquiv.toBialgIso_hom, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, BialgCat.toBialgHom_comp, TensorProduct.rid_tmul, TensorProduct.lid_tmul, HopfAlgebra.mul_antipode_lTensor_comul, CategoryTheory.Iso.toBialgEquiv_toBialgHom, GroupLike.val_pow, CommBialgCat.isoMk_inv, CommBialgCat.forget_map, CommBialgCat.ofHom_id, toLinearMap_comulAlgHom, CommBialgCat.forget₂_commAlgCat_map, BialgHom.ext_of_ring_iff, BialgEquiv.toHopfAlgIso_hom, IsGroupLikeElem.one, CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom, TensorProduct.lid_symm_apply, TensorProduct.rid_toCoalgEquiv, counit_pow, mul_compr₂_comul, BialgCat.forget₂_algebra_obj, CommBialgCat.hom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, BialgEquiv.toHopfAlgIso_inv, CommBialgCat.hom_comp, mul_compr₂_counit, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, BialgCat.MonoidalCategory.inducingFunctorData_εIso, TensorProduct.assoc_symm_tmul, TensorProduct.assoc_toAlgEquiv, isGroupLikeElem_iff_of_mul_eq_one, MonoidAlgebra.mapDomainBialgHom_id, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, BialgEquiv.ofAlgEquiv_apply, BialgEquiv.toBialgIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_injective 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap toAlgebra	—	Function.RightInverse.injective counit_algebraMap
comulAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule toAlgebra Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike comulAlgHom LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra	—	—
comul_algebraMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra RingHom RingHom.instFunLike algebraMap Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra	—	AlgHom.commutes
comul_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Algebra.TensorProduct.instMul Algebra.to_smulCommClass IsScalarTower.right	—	DFunLike.congr_fun TensorProduct.smulCommClass_left smulCommClass_self TensorProduct.isScalarTower IsScalarTower.left Algebra.to_smulCommClass IsScalarTower.right mul_compr₂_comul
comul_natCast 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Algebra.TensorProduct.instAddCommMonoidWithOne	—	map_natCast AlgHomClass.toRingHomClass AlgHom.algHomClass
comul_one 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Algebra.TensorProduct.instOneTensorProduct	—	—
comul_pow 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.instSemiring	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass Algebra.to_smulCommClass IsScalarTower.right RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
counitAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom CommSemiring.toSemiring toAlgebra Algebra.id AlgHom.funLike counitAlgHom LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra	—	—
counitAlgHom_self 📖	mathematical	—	counitAlgHom CommSemiring.toSemiring CommSemiring.toBialgebra AlgHom.id Algebra.id	—	—
counit_algebraMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra RingHom RingHom.instFunLike algebraMap	—	AlgHom.commutes
counit_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	DFunLike.congr_fun Algebra.to_smulCommClass smulCommClass_self IsScalarTower.right IsScalarTower.left mul_compr₂_counit
counit_natCast 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_natCast AlgHomClass.toRingHomClass AlgHom.algHomClass
counit_one 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
counit_pow 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
counit_surjective 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toAlgebra Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra	—	counit_algebraMap
mul_compr₂_comul 📖	mathematical	—	LinearMap.compr₂ CommSemiring.toSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule toAlgebra TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.isScalarTower SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul IsScalarTower.left LinearMap.mul Algebra.to_smulCommClass IsScalarTower.right CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra LinearMap.compl₁₂ Algebra.TensorProduct.instNonUnitalNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra	—	—
mul_compr₂_counit 📖	mathematical	—	LinearMap.compr₂ CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule toAlgebra Semiring.toModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id IsScalarTower.right IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.mul CoalgebraStruct.counit Coalgebra.toCoalgebraStruct toCoalgebra LinearMap.compl₁₂	—	—
nontrivial 📖	mathematical	—	Nontrivial	—	Function.Injective.nontrivial algebraMap_injective
toLinearMap_comulAlgHom 📖	mathematical	—	AlgHom.toLinearMap TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule toAlgebra Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra comulAlgHom CoalgebraStruct.comul Coalgebra.toCoalgebraStruct toCoalgebra	—	—
toLinearMap_counitAlgHom 📖	mathematical	—	AlgHom.toLinearMap CommSemiring.toSemiring toAlgebra Algebra.id counitAlgHom CoalgebraStruct.counit NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Coalgebra.toCoalgebraStruct toCoalgebra	—	—

CommSemiring

Definitions

Name	Category	Theorems
toBialgebra 📖	CompOp	25 math math: BialgCat.rightUnitor_def, Bialgebra.counitBialgHom_apply, BialgCat.tensorUnit_def, AddMonoidAlgebra.mapDomainBialgHom_id, MonoidAlgebra.mapDomainBialgHom_comp, MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom, AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom, Bialgebra.counitBialgHom_self, AddMonoidAlgebra.mapDomainBialgHom_apply, Bialgebra.counitAlgHom_self, MonoidAlgebra.mapDomainBialgHom_apply, Bialgebra.TensorProduct.rid_toAlgEquiv, Bialgebra.counitBialgHom_toCoalgHom, Bialgebra.TensorProduct.lid_toAlgEquiv, AddMonoidAlgebra.mapDomainBialgHom_comp, Bialgebra.TensorProduct.lid_toCoalgEquiv, Bialgebra.TensorProduct.rid_symm_apply, Bialgebra.subsingleton_to_ring, Bialgebra.TensorProduct.rid_tmul, Bialgebra.TensorProduct.lid_tmul, BialgHom.ext_of_ring_iff, BialgCat.leftUnitor_def, Bialgebra.TensorProduct.lid_symm_apply, Bialgebra.TensorProduct.rid_toCoalgEquiv, MonoidAlgebra.mapDomainBialgHom_id

(root)

Definitions

Name	Category	Theorems
Bialgebra 📖	CompData	—

---

← Back to Index