Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-12 15:55 06094d56

View on Github →

feat(linear_algebra/free_module): add class module.free (#7801) We introduce here a new class module.free.

Estimated changes

Created src/linear_algebra/free_module.lean

added def module.free.choose_basis_index

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