## Stream: maths

### Topic: quotient_group.map_mk

#### Kevin Buzzard (Jun 17 2019 at 14:59):

I noticed that I couldn't find the fact that the maps $G\to H\to H/M$ and $G\to G/N\to H/M$ (the latter map being quotient_group.map) were equal in mathlib. So I formalised the statement and then found that the proof was rfl. Does this mean that the lemma should not be in mathlib?

#### Kevin Buzzard (Jun 17 2019 at 14:59):

Here $N$ is a normal subgroup of $G$, $M$ is a normal subgroup of $H$ and we're given $f:G\to H$ with $f(N)\subseteq M$.

#### Johan Commelin (Jun 17 2019 at 15:00):

I guess we might occasionally want to rewrite along that equality. There are lots of things proved by rfl in mathlib.

#### Kevin Buzzard (Jun 17 2019 at 15:00):

I want to rewrite along it right now.

Last updated: May 18 2021 at 08:14 UTC