Theorem LocalizedModule.algebraMap_mk'

Modification history

2023-12-31 14:56

Mathlib/Algebra/Module/LocalizedModule.lean

chore(Algebra.Module.LocalizedModule): use `IsLocalization` instead of `Localization` (#9167) …

Added LocalizedModule.algebraMap_mk'View on Github →