IdrisDoc: Control.Algebra

Control.Algebra

(<->) : Group a => a -> a -> a
Fixity
Left associative, precedence 6
interface AbelianGroup 

Sets equipped with a single binary operation that is associative and
commutative, along with a neutral element for that binary operation and
inverses for all elements. Must satisfy the following laws:

  • Associativity of <+>:
    forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
  • Commutativity of <+>:
    forall a b, a <+> b == b <+> a
  • Neutral for <+>:
    forall a, a <+> neutral == a
    forall a, neutral <+> a == a
  • Inverse for <+>:
    forall a, a <+> inverse a == neutral
    forall a, inverse a <+> a == neutral
interface Field 

Sets equipped with two binary operations – both associative, commutative and
possessing a neutral element – and distributivity laws relating the two
operations. All elements except the additive identity must have a
multiplicative inverse. Must satisfy the following laws:

  • Associativity of <+>:
    forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
  • Commutativity of <+>:
    forall a b, a <+> b == b <+> a
  • Neutral for <+>:
    forall a, a <+> neutral == a
    forall a, neutral <+> a == a
  • Inverse for <+>:
    forall a, a <+> inverse a == neutral
    forall a, inverse a <+> a == neutral
  • Associativity of <.>:
    forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
  • Unity for <.>:
    forall a, a <.> unity == a
    forall a, unity <.> a == a
  • InverseM of <.>, except for neutral
    forall a /= neutral, a <.> inverseM a == unity
    forall a /= neutral, inverseM a <.> a == unity
  • Distributivity of <.> and <+>:
    forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
    forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
inverseM : Field a => (x : a) -> Not (x = neutral) -> a
interface Group 

Sets equipped with a single binary operation that is associative, along with
a neutral element for that binary operation and inverses for all elements.
Must satisfy the following laws:

  • Associativity of <+>:
    forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
  • Neutral for <+>:
    forall a, a <+> neutral == a
    forall a, neutral <+> a == a
  • Inverse for <+>:
    forall a, a <+> inverse a == neutral
    forall a, inverse a <+> a == neutral
inverse : Group a => a -> a
interface Ring 

Sets equipped with two binary operations, one associative and commutative
supplied with a neutral element, and the other associative, with
distributivity laws relating the two operations. Must satisfy the following
laws:

  • Associativity of <+>:
    forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
  • Commutativity of <+>:
    forall a b, a <+> b == b <+> a
  • Neutral for <+>:
    forall a, a <+> neutral == a
    forall a, neutral <+> a == a
  • Inverse for <+>:
    forall a, a <+> inverse a == neutral
    forall a, inverse a <+> a == neutral
  • Associativity of <.>:
    forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
  • Distributivity of <.> and <+>:
    forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
    forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
(<.>) : Ring a => a -> a -> a
Fixity
Left associative, precedence 7
interface RingWithUnity 

Sets equipped with two binary operations, one associative and commutative
supplied with a neutral element, and the other associative supplied with a
neutral element, with distributivity laws relating the two operations. Must
satisfy the following laws:

  • Associativity of <+>:
    forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
  • Commutativity of <+>:
    forall a b, a <+> b == b <+> a
  • Neutral for <+>:
    forall a, a <+> neutral == a
    forall a, neutral <+> a == a
  • Inverse for <+>:
    forall a, a <+> inverse a == neutral
    forall a, inverse a <+> a == neutral
  • Associativity of <.>:
    forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
  • Neutral for <.>:
    forall a, a <.> unity == a
    forall a, unity <.> a == a
  • Distributivity of <.> and <+>:
    forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
    forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
unity : RingWithUnity a => a
mtimes : Monoid a => (n : Nat) -> a -> a

Like stimes, but accepting Z as argument.

pow' : RingWithUnity a => a -> Nat -> a
product' : Foldable t => RingWithUnity a => t a -> a
stimes : Semigroup a => (n : Nat) -> {auto prf : IsSucc n} -> a -> a

Combine n copies of a value with <+>

sum' : Foldable t => Monoid a => t a -> a