Mathlib Map

Structures · Algebra

CoalgEquivClass

CoalgEquivClass F R A B asserts F is a type of bundled coalgebra equivalences from A to B.

Defined in
Mathlib.RingTheory.Coalgebra.Equiv
Shape
4 explicit arguments

Extends2

Extended by1

Concrete types that are instances1

  • CoalgEquiv

How is a type an instance?

Loading the hierarchy index…

Assumed by6

Ancestors6