Submonoid of inverses #
Main definitions #
IsLocalization.invSubmonoid M Sis the submonoid of
S = M⁻¹Rconsisting of inverses of each element
x ∈ M
Implementation notes #
Mathlib/RingTheory/Localization/Basic.lean for a design overview.
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
There is an equivalence of monoids between the image of
There is a canonical map from
1 / x.