simplifty the trivial subgroup

This commit is contained in:
Egbert Rijke 2016-12-01 15:43:05 -05:00
parent de641aac71
commit d3cba4b95d

View file

@ -34,11 +34,8 @@ namespace group
{ intros g p, esimp at *, rewrite p, exact one_inv }
end
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 is_trivial_subgroup (G : Group) (R : subgroup_rel G) : Type :=
(Π g : G, R g → g = 1)
definition full_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u 0} G :=
begin