Def LocalizedModule

Modification history

2025-12-28 17:51

Mathlib/Algebra/Module/LocalizedModule/Basic.lean

chore: unify `LocalizedModule` and `OreLocalization` (#31862) …

Deleted LocalizedModule View on Github →

2023-05-16 18:39

Mathlib/Algebra/Module/LocalizedModule.lean

feat: port Algebra.Module.LocalizedModule (#3993) …

Added LocalizedModule View on Github →