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}}}