Commit 2024-12-27 19:18 f332af85
View on Github →chore(RingTheory/LocalRing): strengthen Module.free_of_flat_of_isLocalRing (#19846)
Make the fact that the proof works with any k-basis of k ⊗[R] M explicit and deduce from this that any generating family contains a basis.