Changes between Version 15 and Version 16 of TypeNats/Interact1


Ignore:
Timestamp:
Dec 19, 2010 6:00:20 PM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Interact1

    v15 v16  
    2626{{{
    2727(m * n ~ k) <=> {m * n == k}
    28 (m * a ~ n) <=> a ~ { n / m }  -- m `divides` n, False otherwise
     28(m * a ~ n) <=> a ~ { n / m }    -- m `divides` n, False otherwise
    2929
    3030(0 * a ~ b) <=> b ~ 0
    3131(1 * a ~ b) <=> a ~ b
    32 (m * a ~ a) <=> a ~ 0                     -- 2 <= m
     32(m * a ~ a) <=> a ~ 0            -- 2 <= m
    3333
    3434(a * b ~ 1) <=> (a ~ 1, b ~ 1)
     
    4242(m ^ n ~ k) <=> {m ^ n == k}
    4343
    44 (m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists
     44(m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists, False otherwise
    4545(1 ^ a ~ b) <=> b ~ 1
    4646(m ^ a ~ a) <=> False           -- m /= 1
    4747
    48 (a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists
     48(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists, False otherwise
    4949(a ^ 0 ~ b) <=> b ~ 1
    5050(a ^ 1 ~ b) <=> a ~ b