next up previous contents
Next: Square Roots Up: The Natural Numbers Previous: Theorems about Plus

Theorems about multiplication

In this file are theorems about multiplication, including those also involving addition e.g. the distributivity laws.

 ** Module lib_nat_times_thms Imports lib_nat_plus_thms
  times_plus_dist_r = ... :
    {i,j,k|nat}Eq (times (plus i j) k) (plus (times i k) (times j k))
  times_plus_dist_l = ... :
    {i,j,k|nat}Eq (times i (plus j k)) (plus (times i j) (times i k))
  times_assoc = ... :
    {i,j,k|nat}Eq (times (times i j) k) (times i (times j k))
  times_zero = ... : {n|nat}Eq zero (times n zero)
  times_one = ... : {n|nat}Eq n (times one n)
  zero_times_lemma = ... :
    {m,n|nat}(Eq zero (times m n))->(Eq zero m \/ Eq zero n)
  one_times_lemma = ... :
    {m,n|nat}(Eq one (times m n))->(Eq one m /\ Eq one n)
  times_commutes = ... : {m,n|nat}Eq (times m n) (times n m)
  times_cancel_right = ... :
    {a,x,y:nat}(Eq (times x (suc a)) (times y (suc a)))->Eq x y
  times_two = ... : {n:nat}Eq (times two n) (plus n n)