Theorem Basis.ofIsLocalizedModule_apply

Modification history

2024-01-10 09:09
Mathlib/RingTheory/Localization/Module.lean
feat: Add Basis.of_isLocalizedModule (#9210) …
Added Basis.ofIsLocalizedModule_applyView on Github →