Commit 2025-04-13 13:07 0f2df1b0

View on Github →

chore(FreeModule): clean up (#23996) Make R and M explicit in Free.exists_basis. Open the Module namespace. Add Free.exists_set as a convenience lemma.

Estimated changes

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

deleted theorem Basis.repr_algebraMap

added theorem Module.Free.Basis.repr_algebraMap

added theorem Module.Free.exists_set

modified theorem Module.Free.of_basis

modified theorem Module.free_def

modified theorem Module.free_iff_set