index of subgroup

Stream: Is there code for X?

[Thomas Browning]

Does mathlib know this:

import group_theory.quotient_group

lemma quotient_group.card_dvd_of_le {G : Type*} [group G] {H K : subgroup G} (h : H ≤ K)
  [fintype (quotient_group.quotient H)] [fintype (quotient_group.quotient K)] :
    fintype.card (quotient_group.quotient K) ∣ fintype.card (quotient_group.quotient H) :=
begin
  sorry,
end

[Johan Commelin]

I'm not aware of it. Relatedly, should we define subgroup.index just to make talking about indices less verbose?
I imagine something like

def subgroup.index (G : Type*) [group G] (H : subgroup G) : nat :=
if nonempty (fintype (quotient_group.quotient H)) then ... else 0

But there might be a smoother definition

[Thomas Browning]

Oh, making it 0 for infinite is a nice touch. Then you can get rid of the fintype assumption on the lemma.

[Thomas Browning]

Trying to resist the urge to call it subgroup.findex

[Mario Carneiro]

what's wrong with just subgroup.index like in Johan's comment?

[Thomas Browning]

It's fine, but we have findim and finrank for this sort of "0 if infinite" thing

[Mario Carneiro]

those seem more likely to be useful when infinite though - I haven't heard of using cardinals for subgroup indexes before

[Thomas Browning]

That's true. We probably wouldn't want to have a separate cardinal-valued subgroup.index