Lines Matching refs:exp
1432 ``complex_exp (z:complex) = exp(RE z) * (cos (IM z),sin (IM z))``);
1434 val _ = overload_on ("exp", Term`$complex_exp`);
1437 ``!x:real. exp (i * x) = (cos x,sin x)``,
1442 ``!z:complex. modu z * exp (i * arg z) = z``,
1447 ``!z:complex w:complex. exp (z + w) = exp z * exp w``,
1452 ``!z:complex. exp (-z) = inv (exp z)``,
1460 ``!z:complex w:complex. exp (z - w) = exp z / exp w``,
1464 ``!z:complex n:num. exp (&n : real * z) = exp z pow n``,
1470 ``!z:complex n:num. exp (&n :complex * z) = exp z pow n``,
1476 ``exp 0c = 1``,
1481 ``!z:complex. exp z <> 0``,
1486 ``!z:complex w:complex. exp (z + w) * exp (-z) = exp w``,
1490 ``!z:complex. exp z * exp (-z) = 1``,
1494 ``!z:complex. exp (-z) * exp z = 1``,