mathlib

9d031be0 - feat(group_theory/congruence): quotients of monoids by congruence relations (#1710)

feat(group_theory/congruence): quotients of monoids by congruence relations (#1710) * add congruence.lean * add has_mul * add definition of congruence relation * minor changes * Tidy up second half of congruence.lean * tidying docstrings * tidying * constructive 3rd isom in setoid used in congruence * remove import * open namespaces earlier * responding to PR comments