Frexlet.Monoid.Commutative.NatSemiLinear.Mult

Properties to do with sums

Definitions

multIsHomomorphism : (a : CommutativeMonoid) -> (n : Nat) -> SetoidHomomorphism (cast a) (cast a) (mult a n)

Totality: total
Visibility: public export

multSetoidHomomorphism : (a : CommutativeMonoid) -> Nat -> cast a ~> cast a

Totality: total
Visibility: public export

multUnit : (a : CommutativeMonoid) -> (x : U a) -> a .rel (the Nat 1 *. x) x

Totality: total
Visibility: public export

multDistributesOverPlusLeft : (a : CommutativeMonoid) -> (n : Nat) -> (m : Nat) -> (x : U a) -> a .rel ((n + m) *. x) ((n *. x) .+. (m *. x))

Totality: total
Visibility: public export

multDistributesOverPlusRight : (a : CommutativeMonoid) -> (n : Nat) -> (x : U a) -> (y : U a) -> a .rel (n *. (x .+. y)) ((n *. x) .+. (n *. y))

Totality: total
Visibility: public export

multPreservation : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> (h : a ~> b) -> (n : Nat) -> (x : U a) -> b .rel ((h .H) .H (n *. x)) (n *. (h .H) .H x)

  NB: a,b are explicit since we can't recover them from the
  homomorphism between them as algebras alone.

Totality: total
Visibility: public export