Theorem Module.Free.of_equiv

Modification history

2026-02-25 05:21
Mathlib/LinearAlgebra/FreeModule/Basic.lean
refactor(Algebra/*): generalize `of_ringEquiv` lemmas (#35351) …
Modified Module.Free.of_equivView on Github →
2023-04-07 13:27
Mathlib/LinearAlgebra/FreeModule/Basic.lean
feat: port LinearAlgebra.FreeModule.Basic (#3317)
Added Module.Free.of_equivView on Github →