Zulip Chat Archive
Stream: mathlib4
Topic: locally free
Kenny Lau (Jun 16 2025 at 09:10):
Which one of this is the current canonical Mathlib4 way to say "locally free"?
Kenny Lau (Jun 16 2025 at 09:11):
(00NX)
Kenny Lau (Jun 16 2025 at 09:11):
or should we make a new typeclass IsLocallyFree R M?
Christian Merten (Jun 16 2025 at 09:12):
Didn't you ask this question already a few weeks ago? My answer was [Module.Projective R M] [Module.Finite R M]
Kenny Lau (Jun 16 2025 at 09:13):
ok, thanks
Last updated: Dec 20 2025 at 21:32 UTC