Commit 2022-11-18 10:29 6be213c4

View on Github →

feat: port Algebra.Homology.ComplexShape (#635) (Not the most useful port at this stage. Just wanted to try some easy file.) mathlib SHA : fd47bdf09e90f553519c712378e651975fe8c829

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/ComplexShape.lean

added def ComplexShape.down'

added theorem ComplexShape.down'_mk

added def ComplexShape.down

added theorem ComplexShape.down_mk

added def ComplexShape.next

added theorem ComplexShape.next_eq'

added def ComplexShape.prev

added theorem ComplexShape.prev_eq'

added def ComplexShape.refl

added def ComplexShape.symm

added theorem ComplexShape.symm_symm

added def ComplexShape.trans

added def ComplexShape.up'

added def ComplexShape.up

added structure ComplexShape