Idris2Doc : Control.Algebra.Laws

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