summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
AgeCommit message (Collapse)Author
2022-04-05Generalise 0 comparison to ≤.Greg Brown
2022-04-05Minor clean up.Greg Brown
2022-04-04Add group inverse preserves identity.Greg Brown
2022-04-04Remove redundant cancel property.Greg Brown
It is in the standard library as `⁻¹-injective`.
2022-04-02Add more properties for ordered structures.Greg Brown
2022-03-21Add some properties of algebraic pseudocode types.Greg Brown