Mathlib v3 is deprecated. Go to Mathlib v4

Theorem module.free_of_finite_type_torsion_free

Modification history

2023-03-02 15:13
src/linear_algebra/free_module/pid.lean
feat(linear_algebra/free_module/pid): rename module.free_of_finite_type_torsion_free (#18537) …
Added module.free_of_finite_type_torsion_freeView on Github →
2021-05-10 07:36
src/linear_algebra/free_module.lean
refactor(*): bundle `is_basis` (#7496) …
Deleted module.free_of_finite_type_torsion_freeView on Github →
2021-04-25 15:13
src/linear_algebra/free_module.lean
feat(linear_algebra): free_of_finite_type_torsion_free (#7341) …
Added module.free_of_finite_type_torsion_freeView on Github →