Theorem LocalizedModule.mk'_smul_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.mk'_smul_mk View on Github →