Idris2Doc : Control.Algebra.Laws

# Control.Algebra.Laws

cancelLeft : {autoconArg : Groupty} -> (x : ty) -> (y : ty) -> (z : ty) -> x<+>y = x<+>z -> y = z
`  y = z if x + y = x + z`

Totality: total
cancelRight : {autoconArg : Groupty} -> (x : ty) -> (y : ty) -> (z : ty) -> y<+>x = z<+>x -> y = z
`  y = z if y + x = z + x.`

Totality: total
groupInverseIsInverseL : {autoconArg : Groupty} -> (x : ty) -> x<+>inversex = neutral
`  Every element has a right inverse.`

Totality: total
homoInverse : {autoconArg : GroupHomomorphismab} -> (x : a) -> theb (to (inversex)) = theb (inverse (tox))
`  Homomorphism preserves inverses.`

Totality: total
homoNeutral : {autoconArg : GroupHomomorphismab} -> toneutral = neutral
`  Homomorphism preserves neutral.`

Totality: total
inverseCommute : {autoconArg : Groupty} -> (x : ty) -> (y : ty) -> y<+>x = neutral -> x<+>y = neutral
`  Inverse elements commute.`

Totality: total
inverseNeutralIsNeutral : {autoconArg : Groupty} -> inverseneutral = neutral
`  -0 = 0`

Totality: total
inverseOfUnityL : {autoconArg : RingWithUnityty} -> (x : ty) -> x<.>inverseunity = inversex
`  x(-1) = -x`

Totality: total
inverseOfUnityR : {autoconArg : RingWithUnityty} -> (x : ty) -> inverseunity<.>x = inversex
`  (-1)x = -x`

Totality: total
inverseSquaredIsIdentity : {autoconArg : Groupty} -> (x : ty) -> inverse (inversex) = x
`  -(-x) = x`

Totality: total
latinSquareProperty : {autoconArg : Groupty} -> (a : ty) -> (b : ty) -> (DPairty (\x => a<+>x = b), DPairty (\y => y<+>a = b))
`  For any a and b, ax = b and ya = b have solutions.`

Totality: total
multInverseInversesL : {autoconArg : Ringty} -> (l : ty) -> (r : ty) -> inversel<.>r = inverse (l<.>r)
`  (-x)y = -(xy)`

Totality: total
multInverseInversesR : {autoconArg : Ringty} -> (l : ty) -> (r : ty) -> l<.>inverser = inverse (l<.>r)
`  x(-y) = -(xy)`

Totality: total
multNegativeByNegativeIsPositive : {autoconArg : Ringty} -> (l : ty) -> (r : ty) -> inversel<.>inverser = l<.>r
`  (-x)(-y) = xy`

Totality: total
multNeutralAbsorbingL : {autoconArg : Ringty} -> (r : ty) -> neutral<.>r = neutral
`  0x = x`

Totality: total
multNeutralAbsorbingR : {autoconArg : Ringty} -> (l : ty) -> l<.>neutral = neutral
`  x0 = 0`

Totality: total
neutralProductInverseL : {autoconArg : Groupty} -> (a : ty) -> (b : ty) -> a<+>b = neutral -> inversea = b
`  ab = 0 -> a^-1 = b`

Totality: total
neutralProductInverseR : {autoconArg : Groupty} -> (a : ty) -> (b : ty) -> a<+>b = neutral -> a = inverseb
`  ab = 0 -> a = b^-1`

Totality: total
selfSquareId : {autoconArg : Groupty} -> (x : ty) -> x<+>x = x -> x = neutral
`  Only identity is self-squaring.`

Totality: total
squareIdCommutative : {autoconArg : Groupty} -> (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 : {autoconArg : MonoidVty} -> (x : ty) -> (y : ty) -> (z : ty) -> y<+>x = neutral -> x<+>z = neutral -> y = z
`  Inverses are unique.`

Totality: total
uniqueSolutionL : {autoconArg : Groupt} -> (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 : {autoconArg : Groupty} -> (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