Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-22 13:52 6e5de190

View on Github →

feat(linear_algebra/free_module): add lemmas (#7950) Easy results about free modules.

Estimated changes

Modified src/algebra/category/Module/projective.lean

Modified src/algebra/module/projective.lean

added theorem module.projective_of_basis

deleted theorem module.projective_of_free

Modified src/linear_algebra/dfinsupp.lean

Modified src/linear_algebra/free_module.lean

Modified src/linear_algebra/std_basis.lean

modified theorem pi.linear_independent_std_basis