Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-20 21:33 c9704ff5

View on Github →

chore(data/matrix, linear_algebra): generalize universe parameters (#3879) @PatrickMassot was complaining that matrix m n R often doesn't work when the parameters are declared as m n : Type* because the universe parameters were equal. This PR makes the universe parameters of m and n distinct where possible, also generalizing some other linear algebra definitions. The types of col and row used to be matrix n punit but are now matrix n unit, otherwise the elaborator can't figure out the universe. This doesn't seem to break anything except for the cases where punit.{n} was explicitly written down. There were some breakages, but the total amount of changes is not too big.

Estimated changes

modified def matrix.col
modified theorem matrix.from_blocks_multiply
modified def matrix.row
modified def matrix
modified theorem matrix.empty_val'
modified theorem matrix.smul_mat_empty
modified theorem dim_eq_of_injective
modified theorem dim_eq_of_surjective
modified theorem dim_le_of_injective
modified theorem dim_le_of_surjective
modified theorem dim_map_le
modified theorem dim_prod
modified theorem dim_range_add_dim_ker
modified theorem dim_range_le
modified theorem dim_range_of_surjective
modified theorem linear_equiv.dim_eq
modified def rank
modified theorem rank_add_le
modified theorem rank_comp_le1
modified theorem rank_comp_le2
modified theorem rank_finset_sum_le
modified theorem rank_le_domain
modified theorem rank_le_range
modified theorem rank_zero
modified theorem matrix.rank_vec_mul_vec