From f84cebe13ce0c77dcaf088e2b2e0317fe549b51d Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Wed, 7 Jun 2017 09:41:41 -0600
Subject: [PATCH] Add product_inl and product_inr.

---
 algebra/product_group.hlean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean
index 63fa749..75c1d66 100644
--- a/algebra/product_group.hlean
+++ b/algebra/product_group.hlean
@@ -61,6 +61,12 @@ namespace group
   infix ` ×g `:60 := group.product
   infix ` ×ag `:60 := group.ab_product
 
+  definition product_inl (G H : Group) : G →g G ×g H :=
+    homomorphism.mk (λx, (x, one)) (λx y, prod_eq !refl !one_mul⁻¹)
+
+  definition product_inr (G H : Group) : H →g G ×g H :=
+    homomorphism.mk (λx, (one, x)) (λx y, prod_eq !one_mul⁻¹ !refl)
+
   definition product_functor [constructor] {G G' H H' : Group} (φ : G →g H) (ψ : G' →g H') :
     G ×g G' →g H ×g H' :=
   homomorphism.mk (λx, (φ x.1, ψ x.2)) (λx y, prod_eq !to_respect_mul !to_respect_mul)