Commit 2023-04-13 17:32 86add5ce

View on Github →

refactor(linear_algebra/matrix/rank): remove decidable_eq arguments (#18800) matrix.to_lin' M is just matrix.vec_mul_lin M with an unused decidability argument. We're a bit close to the tide to risk attempting to do a global replacement, so this just:

Refactors some lemmas about matrix.to_lin' to be first proven about matrix.vec_mul_lin
Changes matrix.rank to be defined in terms of the latter.

Estimated changes

Modified src/data/matrix/rank.lean

modified theorem matrix.rank_eq_finrank_range_to_lin

modified theorem matrix.rank_of_is_unit

modified theorem matrix.rank_one

modified theorem matrix.rank_unit

Modified src/linear_algebra/matrix/to_lin.lean

added theorem matrix.ker_mul_vec_lin_eq_bot_iff

modified def matrix.mul_vec_lin

added theorem matrix.mul_vec_lin_add

added theorem matrix.mul_vec_lin_apply

added theorem matrix.mul_vec_lin_mul

added theorem matrix.mul_vec_lin_one

added theorem matrix.mul_vec_lin_zero

modified theorem matrix.mul_vec_std_basis

modified theorem matrix.mul_vec_std_basis_apply

added theorem matrix.range_mul_vec_lin

added theorem matrix.to_lin'_apply'