macro for division and reciprocal
Major Section:  ACL2-BUILT-INS

See binary-* for multiplication and see unary-/ for reciprocal.

Note that / represents division as follows:

(/ x y)
represents the same term as
(* x (/ y))
which is really
(binary-* x (unary-/ y)).
Also note that / represents reciprocal as follows:
(/ x)
expands to
(unary-/ x).
/ is a Common Lisp macro. See any Common Lisp documentation for more information.