From 22d8fad087f99c411915f24c4693b26db4471444 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Thu, 15 Sep 2016 15:04:10 -0400 Subject: [PATCH] complete is_trivial_subgroup --- algebra/subgroup.hlean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index ac6afd0..9b19f1e 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -22,6 +22,8 @@ namespace group (Rmul : Π{g h}, R g → R h → R (g * h)) (Rinv : Π{g}, R g → R (g⁻¹)) + attribute subgroup_rel.R [coercion] + /-- Every group G has at least two subgroups, the trivial subgroup containing only one, and the full subgroup. --/ definition trivial_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u u} G := begin @@ -32,7 +34,11 @@ namespace group { intros g p, esimp at *, rewrite p, exact one_inv } end - definition is_trivial_subgroup (G : Group) (R : subgroup_rel G) : Prop := sorry /- Π g, R g = trivial_subgroup g -/ + definition is_trivial_subgroup (G : Group) (R : subgroup_rel G) : Prop := + trunctype.mk (Π g : G, R g ↔ trivial_subgroup G g) + begin + apply pi.is_trunc_pi, intro g, apply is_trunc_prod + end definition full_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u 0} G := begin