The localization of a ring at a submonoid: the elements of the submonoid become invertible in the localization.

The natural map from the ring to the localization.

The natural map from the submonoid to the unit group of the localization.

Function extensionality for localisations: two functions are equal if they agree on elements that are coercions.

The field of fractions of an integral domain.