quotient_group.map_mk

Stream: maths

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

I want to rewrite along it right now.