bundled kernels for add_comm_groups?

Stream: maths

[Kevin Buzzard]

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

[Kevin Buzzard]

oh I found them

[Johan Commelin]

Oooh, I didn't know that we had those already.

[Kevin Buzzard]

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

[Kevin Buzzard]

Is there some logic to all of this?

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

So for now the kernel is just a set

[Kevin Buzzard]

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