Theorem LocalizedModule.smul'_mul

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'_mul View on Github →