Mathlib Changelog
v4
Changelog
About
Github
Theorem
Basis.ofIsLocalizedModule_repr_apply
Modification history
2024-01-10 09:09
Mathlib/RingTheory/Localization/Module.lean
feat: Add Basis.of_isLocalizedModule (#9210) …
Added
Basis.ofIsLocalizedModule_repr_apply
View on Github →