Theorem IsLocalizedModule.map_id

Modification history

2025-12-27 16:28
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
chore: tidy various files (#33340)
Modified IsLocalizedModule.map_idView on Github →
2025-12-20 10:21
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
chore(Algebra): fix whitespace (#32906)
Modified IsLocalizedModule.map_idView on Github →
2024-10-29 13:01
Mathlib/Algebra/Module/LocalizedModule.lean
feat(RingTheory/*): prerequisites to the locality of projectivity (#18264) …
Added IsLocalizedModule.map_idView on Github →