Theorem IsLocalizedModule.mk'_smul

Modification history

2026-06-05 17:23

Mathlib/Algebra/Module/LocalizedModule/Basic.lean

feat(Algebra/Module/LocalizedModule): generalize `smul'_mk` (#40196) …

Modified IsLocalizedModule.mk'_smul View on Github →

2023-05-16 18:39

Mathlib/Algebra/Module/LocalizedModule.lean

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

Added IsLocalizedModule.mk'_smul View on Github →