Zulip Chat Archive
Stream: Is there code for X?
Topic: group to group_with_zero
Alex Meiburg (Oct 09 2021 at 22:08):
Given a group G, how do I construct the type consisting of G ∪ {0}, as a group_with_zero?
Kevin Buzzard (Oct 09 2021 at 22:10):
Does with_zero G work? In the sense that if G has a group instance, does with_zero G get a group with zero instance?
Last updated: Dec 20 2023 at 11:08 UTC