- cancelLeft : {auto conArg : Group ty} -> (x : ty) -> (y : ty) -> (z : ty) -> x <+> y = x <+> z -> y = z
y = z if x + y = x + z
Totality: total- cancelRight : {auto conArg : Group ty} -> (x : ty) -> (y : ty) -> (z : ty) -> y <+> x = z <+> x -> y = z
y = z if y + x = z + x.
Totality: total- groupInverseIsInverseL : {auto conArg : Group ty} -> (x : ty) -> x <+> inverse x = neutral
Every element has a right inverse.
Totality: total- homoInverse : {auto conArg : GroupHomomorphism a b} -> (x : a) -> the b (to (inverse x)) = the b (inverse (to x))
Homomorphism preserves inverses.
Totality: total- homoNeutral : {auto conArg : GroupHomomorphism a b} -> to neutral = neutral
Homomorphism preserves neutral.
Totality: total- inverseCommute : {auto conArg : Group ty} -> (x : ty) -> (y : ty) -> y <+> x = neutral -> x <+> y = neutral
Inverse elements commute.
Totality: total- inverseNeutralIsNeutral : {auto conArg : Group ty} -> inverse neutral = neutral
-0 = 0
Totality: total- inverseOfUnityL : {auto conArg : RingWithUnity ty} -> (x : ty) -> x <.> inverse unity = inverse x
x(-1) = -x
Totality: total- inverseOfUnityR : {auto conArg : RingWithUnity ty} -> (x : ty) -> inverse unity <.> x = inverse x
(-1)x = -x
Totality: total- inverseSquaredIsIdentity : {auto conArg : Group ty} -> (x : ty) -> inverse (inverse x) = x
-(-x) = x
Totality: total- latinSquareProperty : {auto conArg : Group ty} -> (a : ty) -> (b : ty) -> (DPair ty (\x => a <+> x = b), DPair ty (\y => y <+> a = b))
For any a and b, ax = b and ya = b have solutions.
Totality: total- multInverseInversesL : {auto conArg : Ring ty} -> (l : ty) -> (r : ty) -> inverse l <.> r = inverse (l <.> r)
(-x)y = -(xy)
Totality: total- multInverseInversesR : {auto conArg : Ring ty} -> (l : ty) -> (r : ty) -> l <.> inverse r = inverse (l <.> r)
x(-y) = -(xy)
Totality: total- multNegativeByNegativeIsPositive : {auto conArg : Ring ty} -> (l : ty) -> (r : ty) -> inverse l <.> inverse r = l <.> r
(-x)(-y) = xy
Totality: total- multNeutralAbsorbingL : {auto conArg : Ring ty} -> (r : ty) -> neutral <.> r = neutral
0x = x
Totality: total- multNeutralAbsorbingR : {auto conArg : Ring ty} -> (l : ty) -> l <.> neutral = neutral
x0 = 0
Totality: total- neutralProductInverseL : {auto conArg : Group ty} -> (a : ty) -> (b : ty) -> a <+> b = neutral -> inverse a = b
ab = 0 -> a^-1 = b
Totality: total- neutralProductInverseR : {auto conArg : Group ty} -> (a : ty) -> (b : ty) -> a <+> b = neutral -> a = inverse b
ab = 0 -> a = b^-1
Totality: total- selfSquareId : {auto conArg : Group ty} -> (x : ty) -> x <+> x = x -> x = neutral
Only identity is self-squaring.
Totality: total- squareIdCommutative : {auto conArg : Group ty} -> (x : ty) -> (y : ty) -> ((a : ty) -> a <+> a = neutral) -> x <+> y = y <+> x
If every square in a group is identity, the group is commutative.
Totality: total- uniqueInverse : {auto conArg : MonoidV ty} -> (x : ty) -> (y : ty) -> (z : ty) -> y <+> x = neutral -> x <+> z = neutral -> y = z
Inverses are unique.
Totality: total- uniqueSolutionL : {auto conArg : Group t} -> (a : t) -> (b : t) -> (x : t) -> (y : t) -> x <+> a = b -> y <+> a = b -> x = y
For any a, b, y, the solution to ya = b is unique.
Totality: total- uniqueSolutionR : {auto conArg : Group ty} -> (a : ty) -> (b : ty) -> (x : ty) -> (y : ty) -> a <+> x = b -> a <+> y = b -> x = y
For any a, b, x, the solution to ax = b is unique.
Totality: total