Equiv

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

Statistics

Metric	Count
Definitions `CoalgEquiv`, `apply`, `symm_apply`, `instEquivLike`, `instFunLike`, `invFun`, `ofBijective`, `ofCoalgHom`, `refl`, `toCoalgHom`, `toCoalgebra`, `toEquiv`, `toLinearEquiv`, `trans`, `CoalgEquivClass`, `instCoeToCoalgEquiv`, `toCoalgEquiv`, `«term_≃ₗc[_]_»`	18
Theorems `apply_symm_apply`, `coe_coe`, `coe_mk`, `coe_ofBijective`, `coe_ofCoalgHom`, `coe_symm_toEquiv`, `coe_symm_toLinearEquiv`, `coe_toCoalgHom`, `coe_toEquiv`, `coe_toEquiv_symm`, `coe_toEquiv_trans`, `coe_toLinearEquiv`, `congr_arg`, `congr_fun`, `ext`, `ext_iff`, `instCoalgEquivClass`, `invFun_eq_symm`, `left_inv`, `ofBijective_apply`, `ofCoalgHom_symm`, `refl_apply`, `refl_symm_apply`, `refl_toCoalgHom`, `refl_toLinearEquiv`, `right_inv`, `symm_apply_apply`, `symm_toCoalgHom`, `symm_toLinearEquiv`, `toCoalgHom_eq_coe`, `toCoalgHom_inj`, `toCoalgHom_injective`, `toEquiv_inj`, `toEquiv_injective`, `toEquiv_symm`, `toLinearEquiv_eq_coe`, `toLinearEquiv_toLinearMap`, `trans_apply`, `trans_symm_apply`, `trans_toCoalgHom`, `trans_toLinearEquiv`, `toCoalgHomClass`, `toSemilinearEquivClass`	43
Total	61

CoalgEquiv

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	26 math math: `coe_toCoalgHom`, `coe_ofCoalgHom`, `toCoalgHom_inj`, `toCoalgHom_eq_coe`, `CategoryTheory.Iso.toCoalgEquiv_toCoalgHom`, `coe_toLinearEquiv`, `trans_apply`, `BialgEquiv.trans_apply`, `coe_coe`, `coe_toEquiv_trans`, `instCoalgEquivClass`, `coe_toEquiv_symm`, `toLinearEquiv_toLinearMap`, `symm_toLinearEquiv`, `symm_toCoalgHom`, `refl_toLinearEquiv`, `coe_symm_toLinearEquiv`, `BialgEquiv.trans_symm_apply`, `refl_toCoalgHom`, `Coalgebra.TensorProduct.lid_toLinearEquiv`, `trans_toLinearEquiv`, `trans_symm_apply`, `Coalgebra.TensorProduct.rid_toLinearEquiv`, `toLinearEquiv_eq_coe`, `Coalgebra.TensorProduct.assoc_toLinearEquiv`, `trans_toCoalgHom`
`instFunLike` 📖	CompOp	34 math math: `coe_toCoalgHom`, `BialgEquiv.refl_symm_apply`, `CategoryTheory.Iso.toCoalgEquiv_toCoalgHom`, `Coalgebra.TensorProduct.lid_tmul`, `refl_apply`, `coe_toLinearEquiv`, `trans_apply`, `coe_coe`, `toCoalgIso_inv`, `ext_iff`, `invFun_eq_symm`, `refl_symm_apply`, `coe_symm_toEquiv`, `Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply`, `coe_toEquiv`, `symm_toCoalgHom`, `coe_mk`, `coe_symm_toLinearEquiv`, `BialgEquiv.trans_symm_apply`, `CommBialgCat.bialgEquivOfIso_symm_apply`, `refl_toCoalgHom`, `Coalgebra.TensorProduct.assoc_tmul`, `Coalgebra.TensorProduct.assoc_symm_tmul`, `trans_symm_apply`, `Coalgebra.TensorProduct.rid_symm_apply`, `symm_apply_apply`, `coe_ofBijective`, `Coalgebra.TensorProduct.rid_tmul`, `apply_symm_apply`, `congr_fun`, `congr_arg`, `Coalgebra.TensorProduct.lid_symm_apply`, `ofBijective_apply`, `toCoalgIso_hom`
`invFun` 📖	CompOp	4 math math: `left_inv`, `BialgEquiv.invFun_eq_symm`, `invFun_eq_symm`, `right_inv`
`ofBijective` 📖	CompOp	2 math math: `coe_ofBijective`, `ofBijective_apply`
`ofCoalgHom` 📖	CompOp	2 math math: `coe_ofCoalgHom`, `ofCoalgHom_symm`
`refl` 📖	CompOp	7 math math: `toCoalgIso_refl`, `refl_apply`, `CategoryTheory.Iso.toCoalgEquiv_refl`, `refl_symm_apply`, `refl_toLinearEquiv`, `refl_toCoalgHom`, `BialgEquiv.refl_toCoalgEquiv`
`toCoalgHom` 📖	CompOp	6 math math: `left_inv`, `toCoalgHom_eq_coe`, `toCoalgHom_injective`, `BialgEquiv.map_mul'`, `trans_toCoalgHom`, `right_inv`
`toCoalgebra` 📖	CompOp	—
`toEquiv` 📖	CompOp	6 math math: `toEquiv_injective`, `toEquiv_inj`, `coe_symm_toEquiv`, `coe_toEquiv_symm`, `coe_toEquiv`, `toEquiv_symm`
`toLinearEquiv` 📖	CompOp	1 math math: `toLinearEquiv_eq_coe`
`trans` 📖	CompOp	8 math math: `trans_apply`, `coe_toEquiv_trans`, `CategoryTheory.Iso.toCoalgEquiv_trans`, `BialgEquiv.trans_toCoalgEquiv`, `trans_toLinearEquiv`, `trans_symm_apply`, `trans_toCoalgHom`, `toCoalgIso_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike` `symm`	—	`LinearEquiv.apply_symm_apply` `RingHomInvPair.ids` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `CoalgHom.funLike` `CoalgHomClass.toCoalgHom` `CoalgEquiv` `EquivLike.toFunLike` `instEquivLike` `CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass` `instFunLike`	—	`CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass`
`coe_mk` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddHom.toFun` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.id` `LinearMap.comp` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `CoalgebraStruct.comul` `LinearMap.toAddHom` `CoalgHom.toLinearMap`	`CoalgEquiv` `instFunLike`	—	`RingHomCompTriple.ids`
`coe_ofBijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `CoalgHom` `CoalgHom.funLike`	`CoalgEquiv` `instFunLike` `ofBijective`	—	—
`coe_ofCoalgHom` 📖	mathematical	`CoalgHom.comp` `CoalgHom.id`	`CoalgHomClass.toCoalgHom` `CoalgEquiv` `EquivLike.toFunLike` `instEquivLike` `CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass` `ofCoalgHom`	—	`CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass`
`coe_symm_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv` `CoalgEquiv` `instFunLike` `symm`	—	—
`coe_symm_toLinearEquiv` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `SemilinearEquivClass.semilinearEquiv` `CoalgEquiv` `instEquivLike` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass` `instFunLike` `symm`	—	`RingHomInvPair.ids` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`
`coe_toCoalgHom` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `CoalgHom.funLike` `CoalgHomClass.toCoalgHom` `CoalgEquiv` `EquivLike.toFunLike` `instEquivLike` `CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass` `instFunLike`	—	`CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass`
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `CoalgEquiv` `instFunLike`	—	—
`coe_toEquiv_symm` 📖	mathematical	—	`Equiv.symm` `toEquiv` `EquivLike.toEquiv` `CoalgEquiv` `instEquivLike` `symm`	—	—
`coe_toEquiv_trans` 📖	mathematical	—	`Equiv.trans` `EquivLike.toEquiv` `CoalgEquiv` `instEquivLike` `trans`	—	—
`coe_toLinearEquiv` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `SemilinearEquivClass.semilinearEquiv` `CoalgEquiv` `instEquivLike` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass` `instFunLike`	—	`RingHomInvPair.ids` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`
`congr_arg` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike`	—	`DFunLike.congr_arg`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike`	—	`DFunLike.congr_fun`
`ext` 📖	—	`DFunLike.coe` `CoalgEquiv` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike`	—	`ext`
`instCoalgEquivClass` 📖	mathematical	—	`CoalgEquivClass` `CoalgEquiv` `instEquivLike`	—	`AddHom.map_add'` `LinearMap.map_smul'` `CoalgHom.counit_comp` `CoalgHom.map_comp_comul`
`invFun_eq_symm` 📖	mathematical	—	`invFun` `DFunLike.coe` `CoalgEquiv` `instFunLike` `symm`	—	—
`left_inv` 📖	mathematical	—	`invFun` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CoalgHom.toLinearMap` `toCoalgHom`	—	—
`ofBijective_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `CoalgHom` `CoalgHom.funLike`	`CoalgEquiv` `instFunLike` `ofBijective`	—	—
`ofCoalgHom_symm` 📖	mathematical	`CoalgHom.comp` `CoalgHom.id`	`symm` `ofCoalgHom`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike` `refl`	—	—
`refl_symm_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike` `symm` `refl`	—	—
`refl_toCoalgHom` 📖	mathematical	—	`CoalgHomClass.toCoalgHom` `CoalgEquiv` `instFunLike` `CoalgEquivClass.toCoalgHomClass` `instEquivLike` `instCoalgEquivClass` `refl` `CoalgHom.id`	—	`CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass`
`refl_toLinearEquiv` 📖	mathematical	—	`SemilinearEquivClass.semilinearEquiv` `CoalgEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instEquivLike` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass` `refl` `LinearEquiv.refl`	—	`RingHomInvPair.ids` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`
`right_inv` 📖	mathematical	—	`invFun` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CoalgHom.toLinearMap` `toCoalgHom`	—	—
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike` `symm`	—	`LinearEquiv.symm_apply_apply` `RingHomInvPair.ids` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`
`symm_toCoalgHom` 📖	mathematical	—	`SemilinearMapClass.semilinearMap` `CoalgHom` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CoalgHomClass.toCoalgHom` `CoalgEquiv` `instFunLike` `CoalgEquivClass.toCoalgHomClass` `instEquivLike` `instCoalgEquivClass` `symm` `CoalgHom.funLike` `CoalgHomClass.toSemilinearMapClass` `CoalgHom.coalgHomClass` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `SemilinearEquivClass.semilinearEquiv` `CoalgEquivClass.toSemilinearEquivClass`	—	`CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass` `CoalgHomClass.toSemilinearMapClass` `CoalgHom.coalgHomClass`
`symm_toLinearEquiv` 📖	mathematical	—	`SemilinearEquivClass.semilinearEquiv` `CoalgEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instEquivLike` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass` `symm` `LinearEquiv.symm`	—	`RingHomInvPair.ids` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`
`toCoalgHom_eq_coe` 📖	mathematical	—	`toCoalgHom` `CoalgHomClass.toCoalgHom` `CoalgEquiv` `EquivLike.toFunLike` `instEquivLike` `CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass`	—	—
`toCoalgHom_inj` 📖	mathematical	—	`CoalgHomClass.toCoalgHom` `CoalgEquiv` `EquivLike.toFunLike` `instEquivLike` `CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass`	—	`toCoalgHom_injective`
`toCoalgHom_injective` 📖	mathematical	—	`CoalgEquiv` `CoalgHom` `toCoalgHom`	—	`toEquiv_injective` `Equiv.ext` `CoalgHom.congr_fun`
`toEquiv_inj` 📖	mathematical	—	`toEquiv`	—	`toEquiv_injective`
`toEquiv_injective` 📖	mathematical	—	`CoalgEquiv` `Equiv` `toEquiv`	—	`CoalgHom.ext` `LinearEquiv.left_inv` `LinearEquiv.right_inv`
`toEquiv_symm` 📖	mathematical	—	`toEquiv` `symm` `Equiv.symm`	—	—
`toLinearEquiv_eq_coe` 📖	mathematical	—	`toLinearEquiv` `SemilinearEquivClass.semilinearEquiv` `CoalgEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instEquivLike` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`	—	`RingHomInvPair.ids`
`toLinearEquiv_toLinearMap` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `SemilinearEquivClass.semilinearEquiv` `CoalgEquiv` `instEquivLike` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass` `SemilinearMapClass.semilinearMap` `CoalgHom` `CoalgHomClass.toCoalgHom` `EquivLike.toFunLike` `CoalgEquivClass.toCoalgHomClass` `CoalgHom.funLike` `CoalgHomClass.toSemilinearMapClass` `CoalgHom.coalgHomClass`	—	`RingHomInvPair.ids` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike` `trans` `EquivLike.toFunLike` `instEquivLike`	—	—
`trans_symm_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgEquiv` `instFunLike` `symm` `trans` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `SemilinearEquivClass.semilinearEquiv` `RingHomInvPair.ids` `instEquivLike` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`	—	—
`trans_toCoalgHom` 📖	mathematical	—	`CoalgHomClass.toCoalgHom` `CoalgEquiv` `EquivLike.toFunLike` `instEquivLike` `CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass` `trans` `CoalgHom.comp` `toCoalgHom`	—	`CoalgEquivClass.toCoalgHomClass` `instCoalgEquivClass`
`trans_toLinearEquiv` 📖	mathematical	—	`SemilinearEquivClass.semilinearEquiv` `CoalgEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instEquivLike` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass` `trans` `LinearEquiv.trans` `RingHomCompTriple.ids`	—	`RingHomInvPair.ids` `CoalgEquivClass.toSemilinearEquivClass` `instCoalgEquivClass`

CoalgEquiv.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

CoalgEquivClass

Definitions

Name	Category	Theorems
`instCoeToCoalgEquiv` 📖	CompOp	—
`toCoalgEquiv` 📖	CompOp	10 math math: `BialgEquiv.toCoalgEquiv_eq_coe`, `BialgEquiv.trans_apply`, `BialgEquiv.symm_toCoalgEquiv`, `BialgEquiv.trans_toCoalgEquiv`, `BialgEquiv.trans_symm_apply`, `Bialgebra.TensorProduct.assoc_toCoalgEquiv`, `Bialgebra.TensorProduct.lid_toCoalgEquiv`, `Bialgebra.TensorProduct.rid_toCoalgEquiv`, `BialgEquiv.refl_toCoalgEquiv`, `BialgEquiv.coe_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCoalgHomClass` 📖	mathematical	—	`CoalgHomClass` `EquivLike.toFunLike`	—	—
`toSemilinearEquivClass` 📖	mathematical	—	`SemilinearEquivClass` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `AddHomClass.map_add` `SemilinearMapClass.toAddHomClass` `CoalgHomClass.toSemilinearMapClass` `toCoalgHomClass` `MulActionSemiHomClass.map_smulₛₗ` `SemilinearMapClass.toMulActionSemiHomClass`

(root)

Definitions

Name	Category	Theorems
`CoalgEquiv` 📖	CompData	52 math math: `CoalgEquiv.coe_toCoalgHom`, `CoalgEquiv.coe_ofCoalgHom`, `CoalgEquiv.toCoalgHom_inj`, `CoalgEquiv.toCoalgHom_eq_coe`, `BialgEquiv.refl_symm_apply`, `CategoryTheory.Iso.toCoalgEquiv_toCoalgHom`, `Coalgebra.TensorProduct.lid_tmul`, `CoalgEquiv.refl_apply`, `CoalgEquiv.coe_toLinearEquiv`, `CoalgEquiv.toCoalgHom_injective`, `CoalgEquiv.toEquiv_injective`, `CoalgEquiv.trans_apply`, `BialgEquiv.trans_apply`, `CoalgEquiv.coe_coe`, `CoalgEquiv.coe_toEquiv_trans`, `CoalgEquiv.toCoalgIso_inv`, `CoalgEquiv.ext_iff`, `CoalgEquiv.instCoalgEquivClass`, `CoalgEquiv.invFun_eq_symm`, `CoalgEquiv.refl_symm_apply`, `CoalgEquiv.coe_symm_toEquiv`, `CoalgEquiv.coe_toEquiv_symm`, `Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply`, `CoalgEquiv.toLinearEquiv_toLinearMap`, `CoalgEquiv.coe_toEquiv`, `CoalgEquiv.symm_toLinearEquiv`, `CoalgEquiv.symm_toCoalgHom`, `CoalgEquiv.coe_mk`, `CoalgEquiv.refl_toLinearEquiv`, `CoalgEquiv.coe_symm_toLinearEquiv`, `BialgEquiv.trans_symm_apply`, `CommBialgCat.bialgEquivOfIso_symm_apply`, `CoalgEquiv.refl_toCoalgHom`, `Coalgebra.TensorProduct.assoc_tmul`, `Coalgebra.TensorProduct.lid_toLinearEquiv`, `Coalgebra.TensorProduct.assoc_symm_tmul`, `CoalgEquiv.trans_toLinearEquiv`, `CoalgEquiv.trans_symm_apply`, `Coalgebra.TensorProduct.rid_symm_apply`, `CoalgEquiv.symm_apply_apply`, `Coalgebra.TensorProduct.rid_toLinearEquiv`, `CoalgEquiv.coe_ofBijective`, `Coalgebra.TensorProduct.rid_tmul`, `CoalgEquiv.toLinearEquiv_eq_coe`, `CoalgEquiv.apply_symm_apply`, `CoalgEquiv.congr_fun`, `Coalgebra.TensorProduct.assoc_toLinearEquiv`, `CoalgEquiv.congr_arg`, `CoalgEquiv.trans_toCoalgHom`, `Coalgebra.TensorProduct.lid_symm_apply`, `CoalgEquiv.ofBijective_apply`, `CoalgEquiv.toCoalgIso_hom`
`CoalgEquivClass` 📖	CompData	2 math math: `BialgEquivClass.toCoalgEquivClass`, `CoalgEquiv.instCoalgEquivClass`
`«term_≃ₗc[_]_»` 📖	CompOp	—

---

← Back to Index