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 NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule 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	DFunLike.coe BialgEquiv Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra instFunLike ofBijective BialgHom BialgHom.funLike	—	—
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 Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule 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	DFunLike.coe BialgEquiv Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra instFunLike ofBijective BialgHom BialgHom.funLike	—	—
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 CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra SemilinearEquivClass.semilinearEquiv BialgEquiv Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra instEquivLike CoalgEquivClass.toSemilinearEquivClass BialgEquivClass.toCoalgEquivClass instBialgEquivClass ofAlgEquiv AlgEquiv AlgEquiv.instEquivLike AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass	—	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