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

Merge branch 'master' of github.com:fpvandoorn/Spectral

Browse source
This commit is contained in:
favonia 2017-06-07 09:38:45 -06:00
commit 95173995f4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
algebra/free_group.hlean
View file

@ -60,10 +60,10 @@ namespace group
end
definition free_group_one [constructor] : FG X := class_of []
definition free_group_inv [unfold 4] : FG X → FG X :=
definition free_group_inv [unfold 3] : FG X → FG X :=
quotient_unary_map (reverse ∘ map sum.flip)
(λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
definition free_group_mul [unfold 4 5] : FG X → FG X → FG X :=
definition free_group_mul [unfold 3 4] : FG X → FG X → FG X :=
quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
section