Theorem Module.Free.of_ringEquiv

Modification history

2026-02-25 05:21
Mathlib/LinearAlgebra/FreeModule/Basic.lean
refactor(Algebra/*): generalize `of_ringEquiv` lemmas (#35351) …
Deleted Module.Free.of_ringEquivView on Github →
2024-11-25 08:40
Mathlib/LinearAlgebra/FreeModule/Basic.lean
feat: the free locus of a (finitely presented) module (#18691)
Added Module.Free.of_ringEquivView on Github →