Idris2Doc : Control.Algebra.Laws

Control.Algebra.Laws

Definitions

uniqueInverse : {auto{conArg:2029} : MonoidVty} -> (x : ty) -> (y : ty) -> (z : ty) ->y<+>x=neutral->x<+>z=neutral->y=z
  Inverses are unique.

Totality: total
Visibility: public export
selfSquareId : {auto{conArg:2147} : Groupty} -> (x : ty) ->x<+>x=x->x=neutral
  Only identity is self-squaring.

Totality: total
Visibility: public export
inverseCommute : {auto{conArg:2247} : Groupty} -> (x : ty) -> (y : ty) ->y<+>x=neutral->x<+>y=neutral
  Inverse elements commute.

Totality: total
Visibility: public export
groupInverseIsInverseL : {auto{conArg:2417} : Groupty} -> (x : ty) ->x<+>inversex=neutral
  Every element has a right inverse.

Totality: total
Visibility: public export
inverseSquaredIsIdentity : {auto{conArg:2459} : Groupty} -> (x : ty) ->inverse (inversex) =x
  -(-x) = x

Totality: total
Visibility: public export
squareIdCommutative : {auto{conArg:2500} : 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
Visibility: public export
inverseNeutralIsNeutral : {auto{conArg:2701} : Groupty} ->inverseneutral=neutral
  -0 = 0

Totality: total
Visibility: public export
cancelLeft : {auto{conArg:2778} : Groupty} -> (x : ty) -> (y : ty) -> (z : ty) ->x<+>y=x<+>z->y=z
  y = z if x + y = x + z

Totality: total
Visibility: public export
cancelRight : {auto{conArg:2923} : Groupty} -> (x : ty) -> (y : ty) -> (z : ty) ->y<+>x=z<+>x->y=z
  y = z if y + x = z + x.

Totality: total
Visibility: public export
neutralProductInverseR : {auto{conArg:3068} : Groupty} -> (a : ty) -> (b : ty) ->a<+>b=neutral->a=inverseb
  ab = 0 -> a = b^-1

Totality: total
Visibility: public export
neutralProductInverseL : {auto{conArg:3129} : Groupty} -> (a : ty) -> (b : ty) ->a<+>b=neutral->inversea=b
  ab = 0 -> a^-1 = b

Totality: total
Visibility: public export
latinSquareProperty : {auto{conArg:3190} : Groupty} -> (a : ty) -> (b : ty) -> ((x : ty**a<+>x=b), (y : ty**y<+>a=b))
  For any a and b, ax = b and ya = b have solutions.

Totality: total
Visibility: public export
uniqueSolutionR : {auto{conArg:3341} : 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
Visibility: public export
uniqueSolutionL : {auto{conArg:3413} : 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
Visibility: public export
homoNeutral : {auto{conArg:3485} : GroupHomomorphismab} ->toneutral=neutral
  Homomorphism preserves neutral.

Totality: total
Visibility: public export
homoInverse : {auto{conArg:3596} : GroupHomomorphismab} -> (x : a) ->theb (to (inversex)) =theb (inverse (tox))
  Homomorphism preserves inverses.

Totality: total
Visibility: public export
multNeutralAbsorbingL : {auto{conArg:3717} : Ringty} -> (r : ty) ->neutral<.>r=neutral
  0x = x

Totality: total
Visibility: public export
multNeutralAbsorbingR : {auto{conArg:3980} : Ringty} -> (l : ty) ->l<.>neutral=neutral
  x0 = 0

Totality: total
Visibility: public export
multInverseInversesL : {auto{conArg:4239} : Ringty} -> (l : ty) -> (r : ty) ->inversel<.>r=inverse (l<.>r)
  (-x)y = -(xy)

Totality: total
Visibility: public export
multInverseInversesR : {auto{conArg:4410} : Ringty} -> (l : ty) -> (r : ty) ->l<.>inverser=inverse (l<.>r)
  x(-y) = -(xy)

Totality: total
Visibility: public export
multNegativeByNegativeIsPositive : {auto{conArg:4577} : Ringty} -> (l : ty) -> (r : ty) ->inversel<.>inverser=l<.>r
  (-x)(-y) = xy

Totality: total
Visibility: public export
inverseOfUnityR : {auto{conArg:4659} : RingWithUnityty} -> (x : ty) ->inverseunity<.>x=inversex
  (-1)x = -x

Totality: total
Visibility: public export
inverseOfUnityL : {auto{conArg:4720} : RingWithUnityty} -> (x : ty) ->x<.>inverseunity=inversex
  x(-1) = -x

Totality: total
Visibility: public export