Commit 2023-04-19 11:04 f0d2fcab

View on Github →

feat: port RingTheory.Localization.Submodule (#3514)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/Submodule.lean

added theorem IsFractionRing.coeSubmodule_injective

added theorem IsFractionRing.coeSubmodule_isPrincipal

added theorem IsFractionRing.coeSubmodule_le_coeSubmodule

added theorem IsFractionRing.coeSubmodule_strictMono

added def IsLocalization.coeSubmodule

added theorem IsLocalization.coeSubmodule_bot

added theorem IsLocalization.coeSubmodule_fg

added theorem IsLocalization.coeSubmodule_injective

added theorem IsLocalization.coeSubmodule_isPrincipal

added theorem IsLocalization.coeSubmodule_le_coeSubmodule

added theorem IsLocalization.coeSubmodule_mono

added theorem IsLocalization.coeSubmodule_mul

added theorem IsLocalization.coeSubmodule_span

added theorem IsLocalization.coeSubmodule_span_singleton

added theorem IsLocalization.coeSubmodule_strictMono

added theorem IsLocalization.coeSubmodule_sup

added theorem IsLocalization.coeSubmodule_top

added theorem IsLocalization.isNoetherianRing

added theorem IsLocalization.mem_coeSubmodule

added theorem IsLocalization.mem_span_iff

added theorem IsLocalization.mem_span_map