Commit 2024-06-23 21:54 f2d04483

View on Github →

feat(RingTheory): localization and finiteness (#14054) We show that Module.Finite is preserved under localizations and that if a module is finite after localizing at a spanning set of elements of the ring, it is finite.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/LocalizedModuleIntegers.lean

added def IsLocalizedModule.IsInteger

added theorem IsLocalizedModule.exist_integer_multiples

added theorem IsLocalizedModule.exist_integer_multiples_of_finite

added theorem IsLocalizedModule.exist_integer_multiples_of_finset

added theorem IsLocalizedModule.exists_integer_multiple

added theorem IsLocalizedModule.finsetIntegerMultiple_image

added theorem IsLocalizedModule.isInteger_add

added theorem IsLocalizedModule.isInteger_smul

added theorem IsLocalizedModule.isInteger_zero

added theorem IsLocalizedModule.map_integerMultiple

added theorem IsLocalizedModule.smul_mem_finsetIntegerMultiple_span

Modified Mathlib/RingTheory/LocalProperties.lean

modified theorem multiple_mem_span_of_mem_localization_span

Created Mathlib/RingTheory/Localization/Finiteness.lean

added theorem Module.Finite.of_isLocalizedModule

added theorem Module.Finite.of_localizationSpan'

added theorem Module.Finite.of_localizationSpan

added theorem Module.Finite.of_localizationSpan_finite'

added theorem Module.Finite.of_localizationSpan_finite