## Stream: maths

### Topic: bundled kernels for add_comm_groups?

#### Kevin Buzzard (Feb 06 2020 at 11:26):

Do we have bundled group homs, kernels etc? I only need them for add_comm_groups.

oh I found them

#### Kevin Buzzard (Feb 06 2020 at 11:27):

They're not in group_theory, they're in algebra/group

#### Kevin Buzzard (Feb 06 2020 at 11:28):

Is there some logic to all of this?

#### Kevin Buzzard (Feb 06 2020 at 11:29):

hmm, maybe we have bundled group homs but not their kernels?

#### Johan Commelin (Feb 06 2020 at 11:34):

We don't have bundled subgroups at the moment, do we?

#### Johan Commelin (Feb 06 2020 at 11:34):

So for now the kernel is just a set

#### Kevin Buzzard (Feb 06 2020 at 11:34):

aah is that what's missing? I'll get a student on it :-)

Last updated: May 11 2021 at 16:22 UTC