Commit 2023-04-07 13:27 03f055b4

View on Github →

feat: port LinearAlgebra.FreeModule.Basic (#3317)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/FreeModule/Basic.lean

added def Module.Free.ChooseBasisIndex

added theorem Module.Free.of_basis

added theorem Module.Free.of_equiv'

added theorem Module.Free.of_equiv

added theorem Module.free_def

added theorem Module.free_iff_set