Control.Algebra.Laws

Definitions

uniqueInverse : {auto {conArg:2029} : MonoidV ty} -> (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} : Group ty} -> (x : ty) -> x <+> x = x -> x = neutral

  Only identity is self-squaring.

Totality: total
Visibility: public export

inverseCommute : {auto {conArg:2247} : Group ty} -> (x : ty) -> (y : ty) -> y <+> x = neutral -> x <+> y = neutral

  Inverse elements commute.

Totality: total
Visibility: public export

groupInverseIsInverseL : {auto {conArg:2417} : Group ty} -> (x : ty) -> x <+> inverse x = neutral

  Every element has a right inverse.

Totality: total
Visibility: public export

inverseSquaredIsIdentity : {auto {conArg:2459} : Group ty} -> (x : ty) -> inverse (inverse x) = x

  -(-x) = x

Totality: total
Visibility: public export

squareIdCommutative : {auto {conArg:2500} : 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
Visibility: public export

inverseNeutralIsNeutral : {auto {conArg:2701} : Group ty} -> inverse neutral = neutral

  -0 = 0

Totality: total
Visibility: public export

cancelLeft : {auto {conArg:2778} : Group ty} -> (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} : Group ty} -> (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} : Group ty} -> (a : ty) -> (b : ty) -> a <+> b = neutral -> a = inverse b

  ab = 0 -> a = b^-1

Totality: total
Visibility: public export

neutralProductInverseL : {auto {conArg:3129} : Group ty} -> (a : ty) -> (b : ty) -> a <+> b = neutral -> inverse a = b

  ab = 0 -> a^-1 = b

Totality: total
Visibility: public export

latinSquareProperty : {auto {conArg:3190} : Group ty} -> (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} : 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
Visibility: public export

uniqueSolutionL : {auto {conArg:3413} : 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
Visibility: public export

homoNeutral : {auto {conArg:3485} : GroupHomomorphism a b} -> to neutral = neutral

  Homomorphism preserves neutral.

Totality: total
Visibility: public export

homoInverse : {auto {conArg:3596} : GroupHomomorphism a b} -> (x : a) -> the b (to (inverse x)) = the b (inverse (to x))

  Homomorphism preserves inverses.

Totality: total
Visibility: public export

multNeutralAbsorbingL : {auto {conArg:3717} : Ring ty} -> (r : ty) -> neutral <.> r = neutral

  0x = x

Totality: total
Visibility: public export

multNeutralAbsorbingR : {auto {conArg:3980} : Ring ty} -> (l : ty) -> l <.> neutral = neutral

  x0 = 0

Totality: total
Visibility: public export

multInverseInversesL : {auto {conArg:4239} : Ring ty} -> (l : ty) -> (r : ty) -> inverse l <.> r = inverse (l <.> r)

  (-x)y = -(xy)

Totality: total
Visibility: public export

multInverseInversesR : {auto {conArg:4410} : Ring ty} -> (l : ty) -> (r : ty) -> l <.> inverse r = inverse (l <.> r)

  x(-y) = -(xy)

Totality: total
Visibility: public export

multNegativeByNegativeIsPositive : {auto {conArg:4577} : Ring ty} -> (l : ty) -> (r : ty) -> inverse l <.> inverse r = l <.> r

  (-x)(-y) = xy

Totality: total
Visibility: public export

inverseOfUnityR : {auto {conArg:4659} : RingWithUnity ty} -> (x : ty) -> inverse unity <.> x = inverse x

  (-1)x = -x

Totality: total
Visibility: public export

inverseOfUnityL : {auto {conArg:4720} : RingWithUnity ty} -> (x : ty) -> x <.> inverse unity = inverse x

  x(-1) = -x

Totality: total
Visibility: public export