feat(group_theory/index): card_mul_index (#10228)

Proves `nat.card H * H.index = nat.card G` as the special case of `K.relindex H * H.index = K.index` when `K = ⊥`.
 


Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/group_theory/index.lean

@@ -147,6 +147,10 @@ by rw [relindex, subgroup_of_bot_eq_top, index_top]
 @[simp, to_additive] lemma relindex_self : H.relindex H = 1 :=
 by rw [relindex, subgroup_of_self, index_top]
 
+@[simp, to_additive card_mul_index] 
+lemma card_mul_index : nat.card H * H.index = nat.card G :=
+by { rw [←relindex_bot_left, ←index_bot], exact relindex_mul_index bot_le }
+
 @[to_additive] lemma index_eq_card [fintype (quotient_group.quotient H)] :
   H.index = fintype.card (quotient_group.quotient H) :=
 nat.card_eq_fintype_card