Idris2Doc : Algebra.Group

Algebra.Group

(source)
Definitions
0 Op1 : Type -> Type
  A unary operation on a type, for instance `negate`.

  Totality: total
  Visibility: public export
0 Op2 : Type -> Type
  A binary operation on a type, for instance `(+)`.

  Totality: total
  Visibility: public export
0 Assoc : Op2 a -> Type
  Proposition that the given binary operation is associative.

  Totality: total
  Visibility: public export
0 Associative : Op2 a -> Type
  Proposition that the given binary operation is associative.

  Totality: total
  Visibility: public export
0 Commutative : Op2 a -> Type
  Proposition that the given binary operation is commutative.

  Totality: total
  Visibility: public export
0 LeftNeutral : a -> Op2 a -> Type
  Proposition that `z` is a left neutral element for the
  given binary operation.

  Totality: total
  Visibility: public export
0 RightNeutral : a -> Op2 a -> Type
  Proposition that `z` is a right neutral element for the
  given binary operation.

  Totality: total
  Visibility: public export
0 LeftInverse : a -> Op1 a -> Op2 a -> Type
  Proposition that `i` is the left inverse of the given binary operation.

  Totality: total
  Visibility: public export
0 RightInverse : a -> Op1 a -> Op2 a -> Type
  Proposition that `i` is the right inverse of the given binary operation.

  Totality: total
  Visibility: public export
rightNeutral : LeftNeutral z p -> Commutative p -> RightNeutral z p
  For a commutative operation, the left neutral element is also a
  right neutral element

  Totality: total
  Visibility: export
leftNeutral : RightNeutral z p -> Commutative p -> LeftNeutral z p
  For a commutative operation, the right neutral element is also a
  left neutral element

  Totality: total
  Visibility: export
rightInverse : LeftInverse z i p -> Commutative p -> RightInverse z i p
  For a commutative operation, the left inverse is also a right inverse.

  Totality: total
  Visibility: export
leftInverse : RightInverse z i p -> Commutative p -> LeftInverse z i p
  For a commutative operation, the right inverse is also a left inverse.

  Totality: total
  Visibility: export
record Semigroup : (a : Type) -> Op2 a -> Type
  A `Semigroup` is a set with a binary associative operation.

  Totality: total
  Visibility: public export
  Constructor: 
MkSemigroup : Associative p -> Semigroup a p

  Projection: 
.associative : Semigroup a p -> Associative p
.associative : Semigroup a p -> Associative p
  Totality: total
  Visibility: public export
associative : Semigroup a p -> Associative p
  Totality: total
  Visibility: public export
record CommutativeSemigroup : (a : Type) -> Op2 a -> Type
  Like a semigroup but the binary operation is also commutative.

  Totality: total
  Visibility: public export
  Constructor: 
MkCommutativeSemigroup : Associative p -> Commutative p -> CommutativeSemigroup a p

  Projections:
  
.associative : CommutativeSemigroup a p -> Associative p
  
.commutative : CommutativeSemigroup a p -> Commutative p
  
.sgrp : CommutativeSemigroup a p -> Semigroup a p
  A commutative semigroup is also a semigroup.
.associative : CommutativeSemigroup a p -> Associative p
  Totality: total
  Visibility: public export
associative : CommutativeSemigroup a p -> Associative p
  Totality: total
  Visibility: public export
.commutative : CommutativeSemigroup a p -> Commutative p
  Totality: total
  Visibility: public export
commutative : CommutativeSemigroup a p -> Commutative p
  Totality: total
  Visibility: public export
.sgrp : CommutativeSemigroup a p -> Semigroup a p
  A commutative semigroup is also a semigroup.

  Totality: total
  Visibility: export
record Monoid : (a : Type) -> a -> Op2 a -> Type
  A `Monoid` is a set with a binary associative operation and a
  neutral element `z` for that operation.

  Totality: total
  Visibility: public export
  Constructor: 
MkMonoid : Associative p -> RightNeutral z p -> LeftNeutral z p -> Monoid a z p

  Projections:
  
.associative : Monoid a z p -> Associative p
  
.leftNeutral : Monoid a z p -> LeftNeutral z p
  
.rightNeutral : Monoid a z p -> RightNeutral z p
  
.sgrp : Monoid a z p -> Semigroup a p
  A monoid is also a semigroup
.associative : Monoid a z p -> Associative p
  Totality: total
  Visibility: public export
associative : Monoid a z p -> Associative p
  Totality: total
  Visibility: public export
.rightNeutral : Monoid a z p -> RightNeutral z p
  Totality: total
  Visibility: public export
rightNeutral : Monoid a z p -> RightNeutral z p
  Totality: total
  Visibility: public export
.leftNeutral : Monoid a z p -> LeftNeutral z p
  Totality: total
  Visibility: public export
leftNeutral : Monoid a z p -> LeftNeutral z p
  Totality: total
  Visibility: public export
.sgrp : Monoid a z p -> Semigroup a p
  A monoid is also a semigroup

  Totality: total
  Visibility: export
record CommutativeMonoid : (a : Type) -> a -> Op2 a -> Type
  Like `Monoid` but with a binary operation that is also commutative.

  Totality: total
  Visibility: public export
  Constructor: 
MkCommutativeMonoid : Associative p -> Commutative p -> LeftNeutral z p -> CommutativeMonoid a z p

  Projections:
  
.associative : CommutativeMonoid a z p -> Associative p
  
.commutative : CommutativeMonoid a z p -> Commutative p
  
.csgrp : CommutativeMonoid a z p -> CommutativeSemigroup a p
  A commutative monoid is also a semigroup
  
.leftNeutral : CommutativeMonoid a z p -> LeftNeutral z p
  
.mon : CommutativeMonoid a z p -> Monoid a z p
  A commutative monoid is also a monoid
  
.rightNeutral : CommutativeMonoid a z p -> RightNeutral z p
  For a commutative monoid, `z` is a right neutral element.
  
.sgrp : CommutativeMonoid a z p -> Semigroup a p
  A commutative monoid is also a semigroup
.associative : CommutativeMonoid a z p -> Associative p
  Totality: total
  Visibility: public export
associative : CommutativeMonoid a z p -> Associative p
  Totality: total
  Visibility: public export
.commutative : CommutativeMonoid a z p -> Commutative p
  Totality: total
  Visibility: public export
commutative : CommutativeMonoid a z p -> Commutative p
  Totality: total
  Visibility: public export
.leftNeutral : CommutativeMonoid a z p -> LeftNeutral z p
  Totality: total
  Visibility: public export
leftNeutral : CommutativeMonoid a z p -> LeftNeutral z p
  Totality: total
  Visibility: public export
mkCommutativeMonoid : ((u : a) -> (v : a) -> (w : a) -> u `p` (v `p` w) = (u `p` v) `p` w) -> ((u : a) -> (v : a) -> u `p` v = v `p` u) -> ((u : a) -> z `p` u = u) -> CommutativeMonoid a z p
  Totality: total
  Visibility: public export
.sgrp : CommutativeMonoid a z p -> Semigroup a p
  A commutative monoid is also a semigroup

  Totality: total
  Visibility: export
.csgrp : CommutativeMonoid a z p -> CommutativeSemigroup a p
  A commutative monoid is also a semigroup

  Totality: total
  Visibility: export
.rightNeutral : CommutativeMonoid a z p -> RightNeutral z p
  For a commutative monoid, `z` is a right neutral element.

  Totality: total
  Visibility: export
.mon : CommutativeMonoid a z p -> Monoid a z p
  A commutative monoid is also a monoid

  Totality: total
  Visibility: export
record Group : (a : Type) -> a -> Op1 a -> Op2 a -> Type
  A `Group` is a monoid with an inverse operation.

  Totality: total
  Visibility: public export
  Constructor: 
MkGroup : Associative p -> LeftNeutral z p -> RightNeutral z p -> LeftInverse z i p -> RightInverse z i p -> Group a z i p

  Projections:
  
.associative : Group a z i p -> Associative p
  
.leftInverse : Group a z i p -> LeftInverse z i p
  
.leftNeutral : Group a z i p -> LeftNeutral z p
  
.mon : Group a z i p -> Monoid a z p
  A group is also a monoid
  
.rightInverse : Group a z i p -> RightInverse z i p
  
.rightNeutral : Group a z i p -> RightNeutral z p
  
.sgrp : Group a z i p -> Semigroup a p
  A group is also a semigroup
.associative : Group a z i p -> Associative p
  Totality: total
  Visibility: public export
associative : Group a z i p -> Associative p
  Totality: total
  Visibility: public export
.leftNeutral : Group a z i p -> LeftNeutral z p
  Totality: total
  Visibility: public export
leftNeutral : Group a z i p -> LeftNeutral z p
  Totality: total
  Visibility: public export
.rightNeutral : Group a z i p -> RightNeutral z p
  Totality: total
  Visibility: public export
rightNeutral : Group a z i p -> RightNeutral z p
  Totality: total
  Visibility: public export
.leftInverse : Group a z i p -> LeftInverse z i p
  Totality: total
  Visibility: public export
leftInverse : Group a z i p -> LeftInverse z i p
  Totality: total
  Visibility: public export
.rightInverse : Group a z i p -> RightInverse z i p
  Totality: total
  Visibility: public export
rightInverse : Group a z i p -> RightInverse z i p
  Totality: total
  Visibility: public export
0 leftInjective : Group a z i p -> u `p` v = u `p` w -> v = w
  In a group, the binary operation is injective when applied
  from the left.

  Totality: total
  Visibility: export
0 solveInverseLeft : Group a z i p -> v `p` u = z -> u = i v
  In a group, from `p v u === z` follows `u === i v`.

  Totality: total
  Visibility: export
0 invertProduct : Group a z i p -> i (u `p` v) = i v `p` i u
  In a group, the inverse of a product is the product of inverses
  (in reverse order).

  Totality: total
  Visibility: export
0 rightInjective : Group a z i p -> v `p` u = w `p` u -> v = w
  In a group, the binary operation is injective when applied
  from the right.

  Totality: total
  Visibility: export
0 solveInverseRight : Group a z i p -> u `p` v = z -> u = i v
  In a group, from `p u v === z` follows `u === i v`.

  Totality: total
  Visibility: export
0 inverseZero : Group a z i p -> i z = z
  In a group, the inverse of the neutral element is
  the neutral element itself.

  Totality: total
  Visibility: export
0 inverseInvolutory : Group a z i p -> i (i u) = u
  In a group, inverting an value twice yields the original value.

  Totality: total
  Visibility: export
.sgrp : Group a z i p -> Semigroup a p
  A group is also a semigroup

  Totality: total
  Visibility: export
.mon : Group a z i p -> Monoid a z p
  A group is also a monoid

  Totality: total
  Visibility: export
record AbelianGroup : (a : Type) -> a -> Op1 a -> Op2 a -> Type
  An abelian group is a group with a commutative binary operation.

  Totality: total
  Visibility: public export
  Constructor: 
MkAbelianGroup : Associative p -> Commutative p -> LeftNeutral z p -> LeftInverse z i p -> AbelianGroup a z i p

  Projections:
  
.associative : AbelianGroup a z i p -> Associative p
  
.cmon : AbelianGroup a z i p -> CommutativeMonoid a z p
  An abelian group is also a commutative monoid
  
.commutative : AbelianGroup a z i p -> Commutative p
  
.csgrp : AbelianGroup a z i p -> CommutativeSemigroup a p
  An abelian group is also a commutative semigroup
  
.grp : AbelianGroup a z i p -> Group a z i p
  An abelian group is also a group
  
.leftInverse : AbelianGroup a z i p -> LeftInverse z i p
  
.leftNeutral : AbelianGroup a z i p -> LeftNeutral z p
  
.mon : AbelianGroup a z i p -> Monoid a z p
  An abelian group is also a monoid
  
.rightInverse : AbelianGroup a z i p -> RightInverse z i p
  For an abelian group, `i` is a right inverse.
  
.rightNeutral : AbelianGroup a z i p -> RightNeutral z p
  For an abelian group, `z` is a right neutral element.
  
.sgrp : AbelianGroup a z i p -> Semigroup a p
  An abelian group is also a semigroup
.associative : AbelianGroup a z i p -> Associative p
  Totality: total
  Visibility: public export
associative : AbelianGroup a z i p -> Associative p
  Totality: total
  Visibility: public export
.commutative : AbelianGroup a z i p -> Commutative p
  Totality: total
  Visibility: public export
commutative : AbelianGroup a z i p -> Commutative p
  Totality: total
  Visibility: public export
.leftNeutral : AbelianGroup a z i p -> LeftNeutral z p
  Totality: total
  Visibility: public export
leftNeutral : AbelianGroup a z i p -> LeftNeutral z p
  Totality: total
  Visibility: public export
.leftInverse : AbelianGroup a z i p -> LeftInverse z i p
  Totality: total
  Visibility: public export
leftInverse : AbelianGroup a z i p -> LeftInverse z i p
  Totality: total
  Visibility: public export
.sgrp : AbelianGroup a z i p -> Semigroup a p
  An abelian group is also a semigroup

  Totality: total
  Visibility: export
.cmon : AbelianGroup a z i p -> CommutativeMonoid a z p
  An abelian group is also a commutative monoid

  Totality: total
  Visibility: export
.csgrp : AbelianGroup a z i p -> CommutativeSemigroup a p
  An abelian group is also a commutative semigroup

  Totality: total
  Visibility: export
.rightNeutral : AbelianGroup a z i p -> RightNeutral z p
  For an abelian group, `z` is a right neutral element.

  Totality: total
  Visibility: export
.rightInverse : AbelianGroup a z i p -> RightInverse z i p
  For an abelian group, `i` is a right inverse.

  Totality: total
  Visibility: export
.mon : AbelianGroup a z i p -> Monoid a z p
  An abelian group is also a monoid

  Totality: total
  Visibility: export
.grp : AbelianGroup a z i p -> Group a z i p
  An abelian group is also a group

  Totality: total
  Visibility: export
0 sgrp_list1 : Semigroup (List1 a) ((a ++))
  Totality: total
  Visibility: export
0 mon_list : Monoid (List a) [] (++)
  Totality: total
  Visibility: export
0 cmon_nat_plus : CommutativeMonoid Nat 0 (+)
  Totality: total
  Visibility: export
0 cmon_nat_mult : CommutativeMonoid Nat 1 (*)
  Totality: total
  Visibility: export
0 appendAssoc : Associative (<+>)
  Totality: total
  Visibility: export
0 appendRightNeutral : RightNeutral Nothing (<+>)
  Totality: total
  Visibility: export
0 mon_maybe : Monoid (Maybe a) Nothing (<+>)
  The default monoid for `Maybe` provided by the prelude:
  Returns the first non-empty value (if any).

  Totality: total
  Visibility: export
union : (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
  Use a binary function to combine two `Maybe`s in case both
  are `Just`s.
  
  This is an associative function, if `p` is associative. It is
  commutative if `p` is commutative.

  Totality: total
  Visibility: public export
0 unionAssoc : Associative p -> Associative (union p)
  Totality: total
  Visibility: export
0 unionCommutative : Commutative p -> Commutative (union p)
  Totality: total
  Visibility: export
0 unionRightNeutral : RightNeutral Nothing (union p)
  Totality: total
  Visibility: export
0 mon_union : Associative p -> Monoid (Maybe a) Nothing (union p)
  Totality: total
  Visibility: export
0 cmon_union : CommutativeSemigroup a p -> CommutativeMonoid (Maybe a) Nothing (union p)
  Totality: total
  Visibility: export
0 appendAssoc : Associative (<+>)
  Totality: total
  Visibility: export
0 appendRightNeutral : RightNeutral EQ (<+>)
  Totality: total
  Visibility: export
0 mon_ordering : Monoid Ordering EQ (<+>)
  The default monoid for `Ordering` provided by the prelude:
  Returns the first non-`EQ` value (if any).

  Totality: total
  Visibility: export
neg : () -> ()
  Totality: total
  Visibility: export
0 appendLeftNeutral : LeftNeutral () (<+>)
  Totality: total
  Visibility: export
0 agrp_unit : AbelianGroup () () neg (<+>)
  The default group for `Unit` provided by the prelude.

  Totality: total
  Visibility: export
0 mon_string : Monoid String "" (++)
  Totality: total
  Visibility: export
0 plus_bits8 : AbelianGroup Bits8 0 negate (+)
  Totality: total
  Visibility: export
0 mult_bits8 : CommutativeMonoid Bits8 1 (*)
  Totality: total
  Visibility: export
0 plus_bits16 : AbelianGroup Bits16 0 negate (+)
  Totality: total
  Visibility: export
0 mult_bits16 : CommutativeMonoid Bits16 1 (*)
  Totality: total
  Visibility: export
0 plus_bits32 : AbelianGroup Bits32 0 negate (+)
  Totality: total
  Visibility: export
0 mult_bits32 : CommutativeMonoid Bits32 1 (*)
  Totality: total
  Visibility: export
0 plus_bits64 : AbelianGroup Bits64 0 negate (+)
  Totality: total
  Visibility: export
0 mult_bits64 : CommutativeMonoid Bits64 1 (*)
  Totality: total
  Visibility: export
0 plus_int8 : AbelianGroup Int8 0 negate (+)
  Totality: total
  Visibility: export
0 mult_int8 : CommutativeMonoid Int8 1 (*)
  Totality: total
  Visibility: export
0 plus_int16 : AbelianGroup Int16 0 negate (+)
  Totality: total
  Visibility: export
0 mult_int16 : CommutativeMonoid Int16 1 (*)
  Totality: total
  Visibility: export
0 plus_int32 : AbelianGroup Int32 0 negate (+)
  Totality: total
  Visibility: export
0 mult_int32 : CommutativeMonoid Int32 1 (*)
  Totality: total
  Visibility: export
0 plus_int64 : AbelianGroup Int64 0 negate (+)
  Totality: total
  Visibility: export
0 mult_int64 : CommutativeMonoid Int64 1 (*)
  Totality: total
  Visibility: export
0 plus_integer : AbelianGroup Integer 0 negate (+)
  Totality: total
  Visibility: export
0 mult_integer : CommutativeMonoid Integer 1 (*)
  Totality: total
  Visibility: export