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