Zulip Chat Archive

Stream: PR reviews

Topic: 2947 normal subgroups


view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 06:39):

#2947 defines normal bundled subgroups. I'm not sure what is the best way to handle it:

  • class subgroup.normal;
  • structure normal_subgroup (with lattice structure etc);
  • predicate subgroup.normal.

Currently the PR defines a predicate with some [fact ] instances. AFAIR, this is not the way fact is supposed to be used.

view this post on Zulip Chris Hughes (Jun 04 2020 at 06:44):

Why is fact not supposed to be used like that. The idea was that we needed it to be a class because of quotients.

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 07:06):

Because Lean will try all fact instances.

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 07:06):

Why not make it @[class] def?

view this post on Zulip Chris Hughes (Jun 04 2020 at 14:26):

I made it an @[class] def. This is what we do with prime ideals, and it seems to work okay for that application.


Last updated: May 06 2021 at 12:15 UTC