G : Type u_2
inst✝¹ : Group G
H✝ K L : Subgroup G
H : Type u_1
inst✝ : Group H
f : G →* H
⊢ Nat.card { x // x ∈ MonoidHom.range f } = Nat.card ↑(Set.range ↑f)
G : Type u_2
inst✝¹ : Group G
H✝ K L : Subgroup G
H : Type u_1
inst✝ : Group H
f : G →* H
⊢ index (MonoidHom.ker f) = Nat.card ↑(Set.range ↑f)
rw [← MonoidHom.comap_bot, index_comap, relindex_bot_left]
no goals
G : Type u_2
inst✝¹ : Group G
H✝ K L : Subgroup G
H : Type u_1
inst✝ : Group H
f : G →* H
⊢ Nat.card { x // x ∈ MonoidHom.range f } = Nat.card ↑(Set.range ↑f)
rfl