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

There have been some changes in the algebra-part of Lean.

Browse source 
We now need to import algebra.bundled in group_theory.basic
This commit is contained in:
Floris van Doorn 2015-12-09 17:12:37 -05:00
parent 633d1f6d46
commit c1d1a5e509
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
group_theory/basic.hlean
View file

@ -10,13 +10,12 @@ Basic group theory
/- /-
Groups are defined in the HoTT library in algebra/group, as part of the algebraic hierarchy. Groups are defined in the HoTT library in algebra/group, as part of the algebraic hierarchy.
However, there is currently no group theory. However, there is currently no group theory.
The only relevant defintions are the trivial group (in types/unit) and some files in algebra/
-/ -/
import algebra.group types.pointed types.pi import types.pointed types.pi algebra.bundled
open eq algebra pointed function is_trunc pi open eq algebra pointed function is_trunc pi
set_option class.force_new true
namespace group namespace group
definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one

1
group_theory/constructions.hlean
View file

@ -10,6 +10,7 @@ import .basic hit.set_quotient types.sigma types.list types.sum
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
equiv equiv
set_option class.force_new true
namespace group namespace group
/- Subgroups -/ /- Subgroups -/