Commit 2024-11-06 09:52 19c566ca

View on Github →

chore: split Algebra.Module.LocalizedModule (#18657)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Algebra/Module/LocalizedModule.lean to Mathlib/Algebra/Module/LocalizedModule/Basic.lean

deleted theorem IsLocalizedModule.map_exact

deleted theorem LocalizedModule.map_exact

deleted theorem isLocalizedModule_iff_isLocalization'

deleted theorem isLocalizedModule_iff_isLocalization

Created Mathlib/Algebra/Module/LocalizedModule/Exact.lean

added theorem IsLocalizedModule.map_exact

added theorem LocalizedModule.map_exact

Renamed Mathlib/Algebra/Module/LocalizedModuleIntegers.lean to Mathlib/Algebra/Module/LocalizedModule/Int.lean

Created Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean

added theorem isLocalizedModule_iff_isLocalization'

added theorem isLocalizedModule_iff_isLocalization

Renamed Mathlib/Algebra/Module/Submodule/Localization.lean to Mathlib/Algebra/Module/LocalizedModule/Submodule.lean

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/LinearAlgebra/Dimension/Localization.lean

Modified Mathlib/RingTheory/Flat/Stability.lean

Modified Mathlib/RingTheory/LocalProperties/Submodule.lean

Modified Mathlib/RingTheory/Localization/Algebra.lean

Modified Mathlib/RingTheory/Localization/Finiteness.lean

Modified Mathlib/RingTheory/Localization/Module.lean

Modified Mathlib/RingTheory/Support.lean