Changes between Version 14 and Version 15 of TypeNats/Interact1


Ignore:
Timestamp:
Dec 19, 2010 5:58:55 PM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Interact1

    v14 v15  
    2626{{{ 
    2727(m * n ~ k) <=> {m * n == k} 
    28 (m * a ~ n) <=> {m / g} * a ~ {n / g}     -- g = gcd m n, 2 <= g 
     28(m * a ~ n) <=> a ~ { n / m }  -- m `divides` n, False otherwise 
    2929 
    3030(0 * a ~ b) <=> b ~ 0 
     
    4141{{{ 
    4242(m ^ n ~ k) <=> {m ^ n == k} 
     43 
    4344(m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists 
     45(1 ^ a ~ b) <=> b ~ 1 
     46(m ^ a ~ a) <=> False           -- m /= 1 
     47 
    4448(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists 
    4549(a ^ 0 ~ b) <=> b ~ 1 
    4650(a ^ 1 ~ b) <=> a ~ b 
    4751(a ^ m ~ a) <=> (a <= 1)        -- 2 <= m 
    48 (1 ^ a ~ b) <=> b ~ 1 
    49 (m ^ a ~ a) <=> False           -- m /= 1 
     52 
    5053}}}