Theorem IsLocalizedModule.injective_of_map_eq

Modification history

2025-02-23 16:13
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
feat(RingTheory/Cotangent): `liftBaseChange` is injective for localizations (#21037) …
Added IsLocalizedModule.injective_of_map_eqView on Github →