G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
hH : Fintype { x // x ∈ H }
⊢ relindex ⊥ H * index H = index ⊥
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
hH : Fintype { x // x ∈ H }
⊢ index H * Fintype.card { x // x ∈ H } = Fintype.card G
rw [← relindex_bot_left_eq_card, ← index_bot_eq_card, mul_comm]
no goals
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
hH : Fintype { x // x ∈ H }
⊢ relindex ⊥ H * index H = index ⊥
exact relindex_mul_index bot_le