Idris2Doc : Frexlet.Monoid.Commutative.Nat

Frexlet.Monoid.Commutative.Nat

CommutativeMonoid structures over the Nats

Reexports

import public Frexlet.Monoid
import public Frexlet.Monoid.Nat

Definitions

Additive : CommutativeMonoid
  Additive commutative monoid structure over the natural numbers

Totality: total
Visibility: public export
Multiplicative : CommutativeMonoid
  Multiplicative monoid structure over the natural numbers

Totality: total
Visibility: public export
multActionNat : (m : Nat) -> (n : Nat) -> m *. n = m * n
Totality: total
Visibility: public export
actionNatCommutative : (m : Nat) -> (n : Nat) -> m *. n = n *. m
Totality: total
Visibility: public export