Idris2Doc : Control.Algebra.Laws

# Control.Algebra.Laws

cancelLeft : {auto {conArg:1822} : Groupty} -> (x : ty) -> (y : ty) -> (z : ty) -> x<+>y = x<+>z -> y = z
y = z if x + y = x + z
Totality: total
cancelRight : {auto {conArg:1947} : Groupty} -> (x : ty) -> (y : ty) -> (z : ty) -> y<+>x = z<+>x -> y = z
y = z if y + x = z + x.
Totality: total
groupInverseIsInverseL : {auto {conArg:1504} : Groupty} -> (x : ty) -> x<+>inversex = neutral
Every element has a right inverse.
Totality: total
homoInverse : {auto {conArg:2494} : GroupHomomorphismab} -> (x : a) -> theb (to (inversex)) = theb (inverse (tox))
Homomorphism preserves inverses.
Totality: total
homoNeutral : {auto {conArg:2390} : GroupHomomorphismab} -> toneutral = neutral
Homomorphism preserves neutral.
Totality: total
inverseCommute : {auto {conArg:1353} : Groupty} -> (x : ty) -> (y : ty) -> y<+>x = neutral -> x<+>y = neutral
Inverse elements commute.
Totality: total
inverseNeutralIsNeutral : {auto {conArg:1752} : Groupty} -> inverseneutral = neutral
-0 = 0
Totality: total
inverseOfUnityL : {auto {conArg:3539} : RingWithUnityty} -> (x : ty) -> x<.>inverseunity = inversex
x(-1) = -x
Totality: total
inverseOfUnityR : {auto {conArg:3486} : RingWithUnityty} -> (x : ty) -> inverseunity<.>x = inversex
(-1)x = -x
Totality: total
inverseSquaredIsIdentity : {auto {conArg:1538} : Groupty} -> (x : ty) -> inverse (inversex) = x
-(-x) = x
Totality: total
latinSquareProperty : {auto {conArg:2162} : 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 : {auto {conArg:3104} : Ringty} -> (l : ty) -> (r : ty) -> inversel<.>r = inverse (l<.>r)
(-x)y = -(xy)
Totality: total
multInverseInversesR : {auto {conArg:3261} : Ringty} -> (l : ty) -> (r : ty) -> l<.>inverser = inverse (l<.>r)
x(-y) = -(xy)
Totality: total
multNegativeByNegativeIsPositive : {auto {conArg:3415} : Ringty} -> (l : ty) -> (r : ty) -> inversel<.>inverser = l<.>r
(-x)(-y) = xy
Totality: total
multNeutralAbsorbingL : {auto {conArg:2605} : Ringty} -> (r : ty) -> neutral<.>r = neutral
0x = x
Totality: total
multNeutralAbsorbingR : {auto {conArg:2856} : Ringty} -> (l : ty) -> l<.>neutral = neutral
x0 = 0
Totality: total
neutralProductInverseL : {auto {conArg:2117} : Groupty} -> (a : ty) -> (b : ty) -> a<+>b = neutral -> inversea = b
ab = 0 -> a^-1 = b
Totality: total
neutralProductInverseR : {auto {conArg:2072} : Groupty} -> (a : ty) -> (b : ty) -> a<+>b = neutral -> a = inverseb
ab = 0 -> a = b^-1
Totality: total
selfSquareId : {auto {conArg:1269} : Groupty} -> (x : ty) -> x<+>x = x -> x = neutral
Only identity is self-squaring.
Totality: total
squareIdCommutative : {auto {conArg:1571} : 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 : {auto {conArg:1175} : MonoidVty} -> (x : ty) -> (y : ty) -> (z : ty) -> y<+>x = neutral -> x<+>z = neutral -> y = z
Inverses are unique.
Totality: total
uniqueSolutionL : {auto {conArg:2343} : 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 : {auto {conArg:2296} : 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