Equiv

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

Statistics

Metric	Count
Definitions BialgEquiv, apply, symm_apply, instEquivLike, instFunLike, ofAlgEquiv, ofBialgHom, ofBijective, refl, toAlgEquiv, toBialgHom, toCoalgEquiv, toEquiv, toMulEquiv, trans, BialgEquivClass, instCoeToBialgEquiv, toBialgEquiv, «term_≃ₐc[_]_»	19
Theorems apply_symm_apply, coe_coe, coe_mk, coe_ofBialgHom, coe_ofBijective, coe_symm_toEquiv, coe_toAlgEquiv, coe_toBialgHom, coe_toCoalgEquiv, coe_toEquiv, coe_toEquiv_symm, coe_toEquiv_trans, comp_symm, congr_arg, congr_fun, ext, ext_iff, instBialgEquivClass, invFun_eq_symm, map_mul', ofAlgEquiv_apply, ofBialgHom_symm, ofBijective_apply, refl_apply, refl_symm_apply, refl_toBialgHom, refl_toCoalgEquiv, symm_apply_apply, symm_comp, symm_toCoalgEquiv, toAlgEquiv_eq_coe, toAlgEquiv_toRingHom, toBialgHom_eq_coe, toBialgHom_inj, toBialgHom_injective, toBialgHom_toAlgHom, toCoalgEquiv_eq_coe, toCoalgEquiv_toCoalgHom, toEquiv_inj, toEquiv_injective, toEquiv_symm, toLinearMap_ofAlgEquiv, toRingEquiv_toRingHom, trans_apply, trans_symm_apply, trans_toBialgHom, trans_toCoalgEquiv, toAlgEquivClass, toBialgHomClass, toCoalgEquivClass, toMulEquivClass	51
Total	70

BialgEquiv

Definitions

Name	Category	Theorems
instEquivLike 📖	CompOp	35 math math: coe_toEquiv_trans, instBialgEquivClass, coe_toBialgHom, toRingEquiv_toRingHom, toCoalgEquiv_eq_coe, symm_comp, coe_toAlgEquiv, trans_apply, toBialgHom_inj, toLinearMap_ofAlgEquiv, toCoalgEquiv_toCoalgHom, Bialgebra.TensorProduct.rid_toAlgEquiv, toAlgEquiv_eq_coe, toAlgEquiv_toRingHom, toBialgHom_eq_coe, coe_toCoalgEquiv, refl_toBialgHom, symm_toCoalgEquiv, coe_ofBialgHom, toBialgHom_toAlgHom, trans_toBialgHom, trans_toCoalgEquiv, trans_symm_apply, Bialgebra.TensorProduct.lid_toAlgEquiv, coe_toEquiv_symm, Bialgebra.TensorProduct.assoc_toCoalgEquiv, Bialgebra.TensorProduct.lid_toCoalgEquiv, CategoryTheory.Iso.toBialgEquiv_toBialgHom, CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom, Bialgebra.TensorProduct.rid_toCoalgEquiv, refl_toCoalgEquiv, comp_symm, coe_mk, Bialgebra.TensorProduct.assoc_toAlgEquiv, coe_coe
instFunLike 📖	CompOp	43 math math: coe_toBialgHom, congr_fun, coe_toEquiv, congr_arg, ext_iff, toRingEquiv_toRingHom, symm_comp, CommBialgCat.bialgEquivOfIso_apply, apply_symm_apply, Bialgebra.TensorProduct.assoc_tmul, invFun_eq_symm, coe_toAlgEquiv, trans_apply, toBialgHom_inj, toCoalgEquiv_toCoalgHom, coe_ofBijective, toAlgEquiv_toRingHom, toBialgHom_eq_coe, coe_toCoalgEquiv, refl_toBialgHom, coe_ofBialgHom, toBialgHom_toAlgHom, trans_toBialgHom, CommBialgCat.isoMk_hom, coe_symm_toEquiv, Bialgebra.TensorProduct.rid_symm_apply, toBialgIso_hom, Bialgebra.TensorProduct.rid_tmul, Bialgebra.TensorProduct.lid_tmul, CategoryTheory.Iso.toBialgEquiv_toBialgHom, CommBialgCat.isoMk_inv, toHopfAlgIso_hom, symm_apply_apply, CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom, Bialgebra.TensorProduct.lid_symm_apply, comp_symm, ofBijective_apply, toHopfAlgIso_inv, Bialgebra.TensorProduct.assoc_symm_tmul, coe_coe, refl_apply, ofAlgEquiv_apply, toBialgIso_inv
ofAlgEquiv 📖	CompOp	2 math math: toLinearMap_ofAlgEquiv, ofAlgEquiv_apply
ofBialgHom 📖	CompOp	2 math math: ofBialgHom_symm, coe_ofBialgHom
ofBijective 📖	CompOp	2 math math: coe_ofBijective, ofBijective_apply
refl 📖	CompOp	8 math math: toHopfAlgIso_refl, toBialgIso_refl, refl_symm_apply, CategoryTheory.Iso.toBialgEquiv_refl, refl_toBialgHom, CategoryTheory.Iso.toHopfAlgEquiv_refl, refl_toCoalgEquiv, refl_apply
toAlgEquiv 📖	CompOp	1 math math: toAlgEquiv_eq_coe
toBialgHom 📖	CompOp	2 math math: toBialgHom_eq_coe, toBialgHom_injective
toCoalgEquiv 📖	CompOp	6 math math: refl_symm_apply, toCoalgEquiv_eq_coe, invFun_eq_symm, map_mul', trans_symm_apply, CommBialgCat.bialgEquivOfIso_symm_apply
toEquiv 📖	CompOp	6 math math: toEquiv_inj, coe_toEquiv, toEquiv_symm, toEquiv_injective, coe_toEquiv_symm, coe_symm_toEquiv
toMulEquiv 📖	CompOp	—
trans 📖	CompOp	9 math math: coe_toEquiv_trans, CategoryTheory.Iso.toHopfAlgEquiv_trans, CategoryTheory.Iso.toBialgEquiv_trans, trans_apply, trans_toBialgHom, trans_toCoalgEquiv, trans_symm_apply, toBialgIso_trans, toHopfAlgIso_trans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_symm_apply 📖	mathematical	—	DFunLike.coe BialgEquiv instFunLike symm	—	Equiv.apply_symm_apply
coe_coe 📖	mathematical	—	DFunLike.coe BialgHom BialgHom.funLike BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass	—	BialgEquivClass.toBialgHomClass instBialgEquivClass
coe_mk 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LinearMap.toAddHom CommSemiring.toSemiring RingHom.id Algebra.toModule CoalgHom.toLinearMap CoalgEquiv.toCoalgHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	CoalgEquivClass.toCoalgEquiv BialgEquiv instEquivLike BialgEquivClass.toCoalgEquivClass instBialgEquivClass	—	BialgEquivClass.toCoalgEquivClass instBialgEquivClass
coe_ofBialgHom 📖	mathematical	BialgHom.comp BialgHom.id	BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass ofBialgHom	—	BialgEquivClass.toBialgHomClass instBialgEquivClass
coe_ofBijective 📖	mathematical	Function.Bijective DFunLike.coe BialgHom Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike	BialgEquiv instFunLike ofBijective	—	—
coe_symm_toEquiv 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toEquiv BialgEquiv instFunLike symm	—	—
coe_toAlgEquiv 📖	mathematical	—	DFunLike.coe AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgEquiv BialgEquiv instEquivLike BialgEquivClass.toAlgEquivClass instBialgEquivClass instFunLike	—	BialgEquivClass.toAlgEquivClass instBialgEquivClass
coe_toBialgHom 📖	mathematical	—	DFunLike.coe BialgHom BialgHom.funLike BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass	—	BialgEquivClass.toBialgHomClass instBialgEquivClass
coe_toCoalgEquiv 📖	mathematical	—	DFunLike.coe AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgEquiv BialgEquiv instEquivLike BialgEquivClass.toAlgEquivClass instBialgEquivClass instFunLike	—	BialgEquivClass.toAlgEquivClass instBialgEquivClass
coe_toEquiv 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toEquiv BialgEquiv instFunLike	—	—
coe_toEquiv_symm 📖	mathematical	—	Equiv.symm toEquiv EquivLike.toEquiv BialgEquiv instEquivLike symm	—	—
coe_toEquiv_trans 📖	mathematical	—	Equiv.trans EquivLike.toEquiv BialgEquiv instEquivLike trans	—	—
comp_symm 📖	mathematical	—	BialgHom.comp BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass symm BialgHom.id	—	BialgHom.coe_algHom_injective BialgEquivClass.toBialgHomClass instBialgEquivClass AlgEquiv.comp_symm
congr_arg 📖	mathematical	—	DFunLike.coe BialgEquiv instFunLike	—	DFunLike.congr_arg
congr_fun 📖	mathematical	—	DFunLike.coe BialgEquiv instFunLike	—	DFunLike.congr_fun
ext 📖	—	DFunLike.coe BialgEquiv instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe BialgEquiv instFunLike	—	ext
instBialgEquivClass 📖	mathematical	—	BialgEquivClass BialgEquiv instEquivLike	—	AddHom.map_add' LinearMap.map_smul' CoalgHom.counit_comp CoalgHom.map_comp_comul map_mul'
invFun_eq_symm 📖	mathematical	—	CoalgEquiv.invFun NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule toCoalgEquiv DFunLike.coe BialgEquiv instFunLike symm	—	—
map_mul' 📖	mathematical	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LinearMap.toAddHom CommSemiring.toSemiring RingHom.id Algebra.toModule CoalgHom.toLinearMap CoalgEquiv.toCoalgHom toCoalgEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
ofAlgEquiv_apply 📖	mathematical	AlgHom.comp CommSemiring.toSemiring Bialgebra.toAlgebra Algebra.id Bialgebra.counitAlgHom AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.TensorProduct.map Bialgebra.comulAlgHom Algebra.TensorProduct.instAlgebra	DFunLike.coe BialgEquiv Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra instFunLike ofAlgEquiv Equiv.toFun AlgEquiv.toEquiv	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass IsScalarTower.to_smulCommClass IsScalarTower.left
ofBialgHom_symm 📖	mathematical	BialgHom.comp BialgHom.id	symm ofBialgHom	—	—
ofBijective_apply 📖	mathematical	Function.Bijective DFunLike.coe BialgHom Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike	BialgEquiv instFunLike ofBijective	—	—
refl_apply 📖	mathematical	—	DFunLike.coe BialgEquiv instFunLike refl	—	—
refl_symm_apply 📖	mathematical	—	DFunLike.coe CoalgEquiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CoalgEquiv.instFunLike CoalgEquiv.symm toCoalgEquiv refl	—	—
refl_toBialgHom 📖	mathematical	—	BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass refl BialgHom.id	—	BialgEquivClass.toBialgHomClass instBialgEquivClass
refl_toCoalgEquiv 📖	mathematical	—	CoalgEquivClass.toCoalgEquiv BialgEquiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instEquivLike BialgEquivClass.toCoalgEquivClass instBialgEquivClass refl CoalgEquiv.refl	—	BialgEquivClass.toCoalgEquivClass instBialgEquivClass
symm_apply_apply 📖	mathematical	—	DFunLike.coe BialgEquiv instFunLike symm	—	Equiv.symm_apply_apply
symm_comp 📖	mathematical	—	BialgHom.comp BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass symm BialgHom.id	—	BialgHom.coe_algHom_injective BialgEquivClass.toBialgHomClass instBialgEquivClass AlgEquiv.symm_comp
symm_toCoalgEquiv 📖	mathematical	—	CoalgEquivClass.toCoalgEquiv BialgEquiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instEquivLike BialgEquivClass.toCoalgEquivClass instBialgEquivClass symm CoalgEquiv.symm	—	BialgEquivClass.toCoalgEquivClass instBialgEquivClass
toAlgEquiv_eq_coe 📖	mathematical	—	toAlgEquiv AlgEquivClass.toAlgEquiv BialgEquiv instEquivLike BialgEquivClass.toAlgEquivClass instBialgEquivClass	—	—
toAlgEquiv_toRingHom 📖	mathematical	—	RingHomClass.toRingHom AlgEquiv AlgEquiv.instFunLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass AlgEquivClass.toAlgEquiv BialgEquiv instEquivLike BialgEquivClass.toAlgEquivClass instBialgEquivClass instFunLike BialgHomClass.toAlgHomClass BialgEquivClass.toBialgHomClass	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass BialgEquivClass.toAlgEquivClass instBialgEquivClass
toBialgHom_eq_coe 📖	mathematical	—	toBialgHom BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass	—	—
toBialgHom_inj 📖	mathematical	—	BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass	—	toBialgHom_injective
toBialgHom_injective 📖	mathematical	—	BialgEquiv BialgHom toBialgHom	—	toEquiv_injective Equiv.ext BialgHom.congr_fun
toBialgHom_toAlgHom 📖	mathematical	—	AlgHomClass.toAlgHom BialgHom BialgHom.funLike BialgHomClass.toAlgHomClass BialgHom.bialgHomClass BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass	—	BialgHomClass.toAlgHomClass BialgHom.bialgHomClass BialgEquivClass.toBialgHomClass instBialgEquivClass
toCoalgEquiv_eq_coe 📖	mathematical	—	toCoalgEquiv CoalgEquivClass.toCoalgEquiv BialgEquiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instEquivLike BialgEquivClass.toCoalgEquivClass instBialgEquivClass	—	—
toCoalgEquiv_toCoalgHom 📖	mathematical	—	CoalgHomClass.toCoalgHom BialgEquiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule EquivLike.toFunLike instEquivLike CoalgEquivClass.toCoalgHomClass BialgEquivClass.toCoalgEquivClass instBialgEquivClass BialgHom BialgHom.funLike BialgHomClass.toCoalgHomClass BialgHom.bialgHomClass BialgHomClass.toBialgHom instFunLike BialgEquivClass.toBialgHomClass	—	CoalgEquivClass.toCoalgHomClass BialgEquivClass.toCoalgEquivClass instBialgEquivClass
toEquiv_inj 📖	mathematical	—	toEquiv	—	toEquiv_injective
toEquiv_injective 📖	mathematical	—	BialgEquiv Equiv toEquiv	—	CoalgEquiv.toEquiv_injective
toEquiv_symm 📖	mathematical	—	toEquiv symm Equiv.symm	—	—
toLinearMap_ofAlgEquiv 📖	mathematical	AlgHom.comp CommSemiring.toSemiring Bialgebra.toAlgebra Algebra.id Bialgebra.counitAlgHom AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.TensorProduct.map Bialgebra.comulAlgHom Algebra.TensorProduct.instAlgebra	LinearEquiv.toLinearMap RingHom.id RingHomInvPair.ids SemilinearEquivClass.semilinearEquiv BialgEquiv Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra instEquivLike CoalgEquivClass.toSemilinearEquivClass BialgEquivClass.toCoalgEquivClass instBialgEquivClass ofAlgEquiv AlgEquivClass.toLinearEquivClass	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass IsScalarTower.to_smulCommClass IsScalarTower.left RingHomInvPair.ids CoalgEquivClass.toSemilinearEquivClass BialgEquivClass.toCoalgEquivClass instBialgEquivClass
toRingEquiv_toRingHom 📖	mathematical	—	RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquivClass.toRingEquiv BialgEquiv instEquivLike AlgEquivClass.toRingEquivClass BialgEquivClass.toAlgEquivClass instBialgEquivClass instFunLike AlgHomClass.toRingHomClass BialgHomClass.toAlgHomClass BialgEquivClass.toBialgHomClass	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass AlgEquivClass.toRingEquivClass BialgEquivClass.toAlgEquivClass instBialgEquivClass
trans_apply 📖	mathematical	—	DFunLike.coe BialgEquiv instFunLike trans CoalgEquiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule EquivLike.toFunLike CoalgEquiv.instEquivLike CoalgEquivClass.toCoalgEquiv instEquivLike	—	—
trans_symm_apply 📖	mathematical	—	DFunLike.coe CoalgEquiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CoalgEquiv.instFunLike CoalgEquiv.symm toCoalgEquiv trans LinearEquiv CommSemiring.toSemiring RingHom.id EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm SemilinearEquivClass.semilinearEquiv RingHomInvPair.ids CoalgEquiv.instEquivLike CoalgEquivClass.toSemilinearEquivClass CoalgEquiv.instCoalgEquivClass CoalgEquivClass.toCoalgEquiv BialgEquiv instEquivLike	—	—
trans_toBialgHom 📖	mathematical	—	BialgHomClass.toBialgHom BialgEquiv instFunLike BialgEquivClass.toBialgHomClass instEquivLike instBialgEquivClass trans BialgHom.comp	—	BialgEquivClass.toBialgHomClass instBialgEquivClass
trans_toCoalgEquiv 📖	mathematical	—	CoalgEquivClass.toCoalgEquiv BialgEquiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instEquivLike BialgEquivClass.toCoalgEquivClass instBialgEquivClass trans CoalgEquiv.trans	—	BialgEquivClass.toCoalgEquivClass instBialgEquivClass

BialgEquiv.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—
symm_apply 📖	CompOp	—

BialgEquivClass

Definitions

Name	Category	Theorems
instCoeToBialgEquiv 📖	CompOp	—
toBialgEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAlgEquivClass 📖	mathematical	—	AlgEquivClass	—	map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass BialgHomClass.toAlgHomClass toBialgHomClass map_add SemilinearMapClass.toAddHomClass CoalgHomClass.toSemilinearMapClass BialgHomClass.toCoalgHomClass AlgHomClass.commutes
toBialgHomClass 📖	mathematical	—	BialgHomClass EquivLike.toFunLike	—	map_add SemilinearMapClass.toAddHomClass CoalgHomClass.toSemilinearMapClass CoalgEquivClass.toCoalgHomClass toCoalgEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass CoalgHomClass.counit_comp CoalgHomClass.map_comp_comul map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MulEquivClass.toMonoidWithZeroHomClass toMulEquivClass map_one MonoidHomClass.toOneHomClass
toCoalgEquivClass 📖	mathematical	—	CoalgEquivClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	—
toMulEquivClass 📖	mathematical	—	MulEquivClass Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—

(root)

Definitions

Name	Category	Theorems
BialgEquiv 📖	CompData	64 math math: BialgEquiv.coe_toEquiv_trans, BialgEquiv.instBialgEquivClass, BialgEquiv.coe_toBialgHom, BialgEquiv.congr_fun, BialgEquiv.coe_toEquiv, BialgEquiv.congr_arg, BialgEquiv.ext_iff, CommBialgCat.isoEquivBialgEquiv_apply, BialgEquiv.toRingEquiv_toRingHom, BialgEquiv.toCoalgEquiv_eq_coe, BialgEquiv.symm_comp, CommBialgCat.bialgEquivOfIso_apply, BialgEquiv.apply_symm_apply, Bialgebra.TensorProduct.assoc_tmul, BialgEquiv.invFun_eq_symm, BialgEquiv.coe_toAlgEquiv, BialgEquiv.trans_apply, BialgEquiv.toBialgHom_inj, BialgEquiv.toLinearMap_ofAlgEquiv, BialgEquiv.toCoalgEquiv_toCoalgHom, Bialgebra.TensorProduct.rid_toAlgEquiv, BialgEquiv.toAlgEquiv_eq_coe, CommBialgCat.isoEquivBialgEquiv_symm_apply, BialgEquiv.coe_ofBijective, BialgEquiv.toEquiv_injective, BialgEquiv.toAlgEquiv_toRingHom, BialgEquiv.toBialgHom_eq_coe, BialgEquiv.toBialgHom_injective, BialgEquiv.coe_toCoalgEquiv, BialgEquiv.refl_toBialgHom, BialgEquiv.symm_toCoalgEquiv, BialgEquiv.coe_ofBialgHom, BialgEquiv.toBialgHom_toAlgHom, BialgEquiv.trans_toBialgHom, BialgEquiv.trans_toCoalgEquiv, BialgEquiv.trans_symm_apply, Bialgebra.TensorProduct.lid_toAlgEquiv, BialgEquiv.coe_toEquiv_symm, CommBialgCat.isoMk_hom, BialgEquiv.coe_symm_toEquiv, Bialgebra.TensorProduct.assoc_toCoalgEquiv, Bialgebra.TensorProduct.lid_toCoalgEquiv, Bialgebra.TensorProduct.rid_symm_apply, BialgEquiv.toBialgIso_hom, Bialgebra.TensorProduct.rid_tmul, Bialgebra.TensorProduct.lid_tmul, CategoryTheory.Iso.toBialgEquiv_toBialgHom, CommBialgCat.isoMk_inv, BialgEquiv.toHopfAlgIso_hom, BialgEquiv.symm_apply_apply, CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom, Bialgebra.TensorProduct.lid_symm_apply, Bialgebra.TensorProduct.rid_toCoalgEquiv, BialgEquiv.refl_toCoalgEquiv, BialgEquiv.comp_symm, BialgEquiv.ofBijective_apply, BialgEquiv.toHopfAlgIso_inv, BialgEquiv.coe_mk, Bialgebra.TensorProduct.assoc_symm_tmul, Bialgebra.TensorProduct.assoc_toAlgEquiv, BialgEquiv.coe_coe, BialgEquiv.refl_apply, BialgEquiv.ofAlgEquiv_apply, BialgEquiv.toBialgIso_inv
BialgEquivClass 📖	CompData	1 math math: BialgEquiv.instBialgEquivClass
«term_≃ₐc[_]_» 📖	CompOp	—

---

← Back to Index