Submodules in localizations of commutative rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Implementation notes #
src/ring_theory/localization/basic.lean for a design overview.
localization, ring localization, commutative ring localization, characteristic predicate,
commutative ring, field of fractions
Map from ideals of
R to submodules of
S induced by