Declares multiplicative inversion of a real number to be a primitive function symbol. It is characterized by axioms rather than given by a definition.