Infinite groups and cardinal

Stream: general

[Anatole Dedecker]

Just wondering : is there any interest in generalizing cardinality results about finite groups (for exemple docs#subgroup.card_subgroup_dvd_card) to infinite groups using docs#cardinal, or is it useless because no one uses infinite cardinals in group theory anyway ?

[Floris van Doorn]

assuming the axiom of choice, divisibility on infinite cardinals coincides with ≤, right?

[Floris van Doorn]

So at least this particular result doesn't seem useful for infinite groups.

[Mario Carneiro]

For the infinite cardinal case, docs#add_subgroup.add_group_equiv_quotient_times_add_subgroup is likely to be more useful anyway