From 304bcc472a3ec532d55f756a643d40ac5b9d4828 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 10 Dec 2015 18:37:30 -0500
Subject: [PATCH] homework accomplished

---
 group_theory/constructions.hlean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/group_theory/constructions.hlean b/group_theory/constructions.hlean
index 2e1b242..7f017b8 100644
--- a/group_theory/constructions.hlean
+++ b/group_theory/constructions.hlean
@@ -631,5 +631,24 @@ namespace group
     Rinv := kernel_inv φ
   ⦄
 
+  definition kernel_subgroup_isnormal (φ : G₁ →g G₂) (g : G₁) (h : G₁) : kernel φ g → kernel φ (h * g * h⁻¹) :=
+  begin
+    esimp at *,
+    intro p,
+    exact calc
+      φ (h * g * h⁻¹) = (φ (h * g)) * φ (h⁻¹)   : respect_mul
+                  ... = (φ h) * (φ g) * (φ h⁻¹) : respect_mul
+                  ... = (φ h) * 1 * (φ h⁻¹)     : p
+                  ... = (φ h) * (φ h⁻¹)         : mul_one
+                  ... = (φ h) * (φ h)⁻¹         : respect_inv
+                  ... = 1                       : mul.right_inv
+  end
+
+  definition kernel_normal_subgroup (φ : G₁ →g G₂) : normal_subgroup_rel G₁ :=
+  ⦃ normal_subgroup_rel,
+    kernel_subgroup φ,
+    is_normal := kernel_subgroup_isnormal φ
+  ⦄
+
   end kernels
 end group