michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

defined the full subgoup in group_basic.hlean

Browse source
This commit is contained in:
Egbert Rijke 2016-09-08 14:27:51 -04:00
parent b470ea7dcd
commit b1dfa3ad7b
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
algebra/group_basics.hlean
View file

@ -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 -/