Theorem IsLocalizedModule.mk'_mul_mk'_of_map_mul
Modification history
2025-04-08 22:12
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
feat: generalize Mathlib.Algebra.Algebra + Module (#23190) …
Modified IsLocalizedModule.mk'_mul_mk'_of_map_mulView on Github →