Zulip Chat Archive

Stream: general

Topic: what is the purpose of is_subgroup

Kenny Lau (Mar 31 2018 at 19:55):

what is the purpose of is_subgroup if you don't prove that they are groups?

Kenny Lau (Mar 31 2018 at 20:15):

@Kevin Buzzard

Kevin Buzzard (Apr 01 2018 at 16:42):

I give up.

Kenny Lau (Apr 03 2018 at 03:55):

@Mario Carneiro should I prove it?

Mario Carneiro (Apr 03 2018 at 03:55):

sure

Kenny Lau (Apr 03 2018 at 03:56):

I guess we will wait until mathlib builds?

Mario Carneiro (Apr 03 2018 at 04:08):

WIP

Last updated: Dec 20 2023 at 11:08 UTC