Stream: new members

Topic: Achievement: cardinality of subgroups of infinite groups

Pedro Minicz (Jun 12 2020 at 00:46):

Another personal achievement/code review thread. Today I formalized the following: let G be an infinite group and H a subgroup s.t. #H < #G, then #G/H = #G.

The code is on Gist.

Pedro Minicz (Jun 12 2020 at 00:47):

I am pretty sure this isn't on mathlib, if it is I just missed it really hard. :grinning_face_with_smiling_eyes:

Kevin Buzzard (Jun 12 2020 at 00:50):

I think #(G/H) * #H = #G is in mathlib (perhaps in a stronger form of a bijection given a choice of a set of reps). Assuming AC your result probably follows from that.

Kenny Lau (Jun 12 2020 at 06:52):

yeah because if #G/H < #G then #G/H * #H = max(#G/H, #H) < #G

Assuming LEM ;-)

Pedro Minicz (Jun 12 2020 at 15:14):

#G/H * #H = #G is in mathlib as group_equiv_quotient_times_subgroup.

Pedro Minicz (Jun 12 2020 at 15:15):

I think the should be a simpler way of achieving this result. The proof itself is quite simple, but the code to do is turned out a bit convoluted.

Last updated: May 16 2021 at 21:11 UTC