yellowsquid/helium.git/src/Helium/Algebra/Ordered/StrictTotal, branch master [no description] http://git.yellowsquid.uk/yellowsquid/helium.git/atom?h=master 2022-04-09T15:24:18Z Add some more algebraic properties. 2022-04-09T15:24:18Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-09T15:24:18Z urn:sha1:c6aee22d68aa614619cecc08a15332294a9de0de Add another tiny proof. 2022-04-05T12:16:57Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-05T12:16:57Z urn:sha1:e2b91853b58c57b8ad616e728bc55e3570490343 Add a useful transport proof. 2022-04-05T11:43:53Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-05T11:43:53Z urn:sha1:7de7db24ba5bb2cfe9fae6f070e60db3510fcc69 Add commutativity of reciprocal and power. 2022-04-05T11:11:41Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-05T11:11:41Z urn:sha1:2f4a5a56437837cc90c9043131764513472347df Add properties of multiplying to 0. 2022-04-05T11:10:47Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-05T11:10:47Z urn:sha1:b75264cfcc2e2b9a999205acda93353ded1b9cfe Generalise 0 comparison to ≤. 2022-04-05T11:08:00Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-05T11:08:00Z urn:sha1:038d2109e78d9c688acfc3338140cc908151db76 Minor clean up. 2022-04-05T11:06:33Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-05T11:06:33Z urn:sha1:b212c150ec0a9bf45cf6c28fba997693669e78d2 Add some more ordered division ring properties. 2022-04-04T14:51:22Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-04T14:51:22Z urn:sha1:6acd0e87fa8ab2a3230626b37f1cd02181810a1a Add group inverse preserves identity. 2022-04-04T14:40:31Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-04T14:40:31Z urn:sha1:4cd820506e0fd2a5595a11555fc2a6206757b3cd Generalise the precondition for 0 < 1 in rings. 2022-04-04T11:39:22Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-04T11:39:22Z urn:sha1:dc2c15ebc9c494b45e8f6c8435752fcb0a66bd3a