summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra/Ordered/StrictTotal
AgeCommit message (Expand)Author
2022-04-05Add a useful transport proof.Greg Brown
2022-04-05Add commutativity of reciprocal and power.Greg Brown
2022-04-05Add properties of multiplying to 0.Greg Brown
2022-04-05Generalise 0 comparison to ≤.Greg Brown
2022-04-05Minor clean up.Greg Brown
2022-04-04Add some more ordered division ring properties.Greg Brown
2022-04-04Add group inverse preserves identity.Greg Brown
2022-04-04Generalise the precondition for 0 < 1 in rings.Greg Brown
2022-04-04Remove redundant cancel property.Greg Brown
2022-04-02Add some properties of ordered fields.Greg Brown
2022-04-02Add more properties for ordered structures.Greg Brown
2022-03-21Add some properties of algebraic pseudocode types.Greg Brown
2022-03-21Add missing renamings.Greg Brown
2022-01-18Define the semantics of pseudocode data types.Greg Brown
2022-01-16Define ordered algebraic structures.Greg Brown