fpvandoorn / lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)
Apache License 2.0
0 stars 0 forks source link

change definition of graded morphism #10

Closed fpvandoorn closed 6 years ago

fpvandoorn commented 6 years ago

the degree d should satisfy d g = d 0 + g and should be defined on an abelian group.