Theorem IsLocalizedModule.linearMap_ext

Modification history

2024-12-07 06:05
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
feat(RingTheory/LocalProperties): flatness is a local property (#19085) …
Added IsLocalizedModule.linearMap_extView on Github →