Achievement: cardinality of subgroups of infinite groups

Stream: new members

[Pedro Minicz]

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]

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]

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]

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

[Kevin Buzzard]

Assuming LEM ;-)

[Pedro Minicz]

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

[Pedro Minicz]

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.