A cardinality criterion for group isomorphism

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem MonoidHom.nonempty_mulEquiv_iff_card_eq {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite H] (φ : G →* H) (hφ : Function.Injective ⇑φ) : Nonempty (G ≃* H) ↔ Nat.card G = Nat.card H

Between finite groups, an injective homomorphism extends to an isomorphism iff the two groups have the same cardinality.