Zulip Chat Archive

Stream: PR reviews

Topic: 2947 normal subgroups

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.

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.

Yury G. Kudryashov (Jun 04 2020 at 07:06):

Because Lean will try all fact instances.

Yury G. Kudryashov (Jun 04 2020 at 07:06):

Why not make it @[class] def?

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: Dec 20 2023 at 11:08 UTC