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

tiny change

Browse source
This commit is contained in:
Steve Awodey 2017-02-16 21:10:44 -05:00
parent 92a4b95302
commit 2aaea21e2a
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
algebra/exact_couple.hlean
View file

@ -63,7 +63,7 @@ definition right_extend_hom_SES {A B C A' B' C' : AbGroup}
exact right_extend_SES ses ses' hA hB htpy1,
exact htpy1,
exact sorry -- fapply quotient_group_compute,
end
definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1