Zulip Chat Archive

Stream: maths

Topic: quotient_group.map_mk


view this post on Zulip Kevin Buzzard (Jun 17 2019 at 14:59):

I noticed that I couldn't find the fact that the maps GHH/MG\to H\to H/M and GG/NH/MG\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?

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 14:59):

Here NN is a normal subgroup of GG, MM is a normal subgroup of HH and we're given f:GHf:G\to H with f(N)Mf(N)\subseteq M.

view this post on Zulip 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.

view this post on Zulip 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