proposition: Proposition grp_prod_corec {G H K : Group} (f : GroupHomomorphism K G) (g : GroupHomomorphism K H) : GroupHomomorphism K (grp_prod G H).
proof: Proof. snrapply Build_GroupHomomorphism. - exact (fun x:K => (f x, g x)). - intros x y. refine (path_prod' _ _ ); try apply grp_homo_op. Defined.
imports: Basics Types HProp HFiber HSet PathAny (notations) Classes.interfaces.abstract_algebra (hints) Classes.interfaces.abstract_algebra (hints) Classes.interfaces.canonical_names Classes.interfaces.canonical_names (SgOp, sg_op, One, one, MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity, Negate, negate, Associative, simple_associativity, associativity, LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity) Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, negate_l, negate_r, IsSemiGroup(..), sg_set, sg_ass, IsMonoid(..), monoid_left_id, monoid_right_id, monoid_semigroup, IsMonoidPreserving(..), monmor_unitmor, monmor_sgmor, IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit) Classes.theory.groups Pointed.Core WildCat Spaces.Nat.Core Truncations.Core