Stream: new members
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
Kevin Buzzard (Jun 12 2020 at 07:44):
Assuming LEM ;-)
Pedro Minicz (Jun 12 2020 at 15:14):
#G/H * #H = #G is in mathlib as
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