Commit 2023-04-12 09:52 b5b5dd5a

View on Github →

feat(linear_algebra/free_module/finite/rank): remove module.free assumption (#18792) Combined with the result in #18787, this lets us golf a downstream proof about matrices.

Estimated changes

Modified src/data/matrix/rank.lean

Modified src/linear_algebra/dimension.lean

added theorem linear_independent_le_span_finset

Modified src/linear_algebra/free_module/finite/rank.lean

modified theorem linear_map.finrank_le_finrank_of_injective

modified theorem linear_map.finrank_range_le

modified theorem submodule.finrank_le

modified theorem submodule.finrank_quotient_le