From f826a7a7114bb454d7d559564898346090cb0b95 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Thu, 15 Sep 2016 15:06:54 -0400 Subject: [PATCH] complete is_full_subgroup --- algebra/subgroup.hlean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index 9b19f1e..4781e99 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -49,7 +49,8 @@ namespace group { intros g p, esimp, constructor } end - definition is_full_subgroup (G : Group) (R : subgroup_rel G) : Prop := sorry /- Π g, R g -/ + definition is_full_subgroup (G : Group) (R : subgroup_rel G) : Prop := + trunctype.mk' -1 (Π g : G, R g) /-- Every group homomorphism f : G -> H determines a subgroup of H, the image of f, and a subgroup of G, the kernel of f. In the following definition we define the image of f. Since a subgroup is required to be closed under the group operations, showing that the image of f is closed under the group operations is part of the definition of the image of f. --/