## 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: May 06 2021 at 12:15 UTC