theorem GroupHomomorphisms.mul_preserving_map_one {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G → G') (hf : ∀ (a b : G), f (a * b) = f a * f b) : f 1 = 1

theorem GroupHomomorphisms.mul_preserving_map_inv {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G → G') (hf : ∀ (a b : G), f (a * b) = f a * f b) (a : G) : f a⁻¹ = (f a)⁻¹

theorem GroupHomomorphisms.mul_preserving_map_properties {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G → G') (hf : ∀ (a b : G), f (a * b) = f a * f b) : f 1 = 1 ∧ ∀ (a : G), f a⁻¹ = (f a)⁻¹

def GroupHomomorphisms.GroupHomomorphism (G : Type u_3) (G' : Type u_4) [Group G] [Group G'] : Type (max u_3 u_4)

theorem GroupHomomorphisms.card_eq_card_ker_mul_card_range {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] [Fintype G] [Fintype G'] (f : G →* G') [Fintype ↥f.ker] [Fintype ↥f.range] : Fintype.card G = Fintype.card ↥f.ker * Fintype.card ↥f.range