# Maths in Lean : quotients and equivalence classes

A type with an equivalence relation on it is called a `setoid`

in Lean. Setoids are defined in `init/data/setoid.lean`

and the quotient type corresponding to the equivalence classes of the equivalence relation is defined in `init/data/quot.lean`

. The online document Theorem Proving In Lean has quite a good section about setoids and quotients[external link].

TODO: find a nice equivalence relation in mathlib (quotient groups? congruences mod n?) and give it as an example here.

### Like this:

Like Loading...