G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex ⊥ H * index H = index ⊥
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ Nat.card { x // x ∈ H } * index H = Nat.card G
rw [← relindex_bot_left, ← index_bot]
no goals
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex ⊥ H * index H = index ⊥
exact relindex_mul_index bot_le