Theorem LocalizedModule.smul_def

Modification history

2023-12-31 14:56

Mathlib/Algebra/Module/LocalizedModule.lean

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

Added LocalizedModule.smul_def View on Github →