From b1dfa3ad7bb292551d20fec0d9daf76cdb8eec70 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 8 Sep 2016 14:27:51 -0400 Subject: [PATCH] defined the full subgoup in group_basic.hlean --- algebra/group_basics.hlean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/algebra/group_basics.hlean b/algebra/group_basics.hlean index 0154598..3e48db4 100644 --- a/algebra/group_basics.hlean +++ b/algebra/group_basics.hlean @@ -36,7 +36,11 @@ namespace group definition full_subgroup (G : Group) : subgroup_rel G := begin - exact sorry /- λ g, unit -/ + fapply subgroup_rel.mk, + { intro g, fapply trunctype.mk, exact g = g, exact _}, + { esimp }, + { intros g h p q, esimp }, + { intros g p, esimp } end definition is_full_subgroup (G : Group) (R : subgroup_rel G) : Prop := sorry /- Π g, R g -/