Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 00:00 6c351a8f

View on Github →

refactor(data/matrix/basic): add matrix.of for type casting (#14992) Without this, it is easier to get confused between matrix and pi types, which have different multiplication operators. With this in place, we can have a special matrix notation that actually produces terms of type matrix.

Estimated changes

modified def matrix.map
added theorem matrix.neg_of
added def matrix.of
added theorem matrix.of_add_of
added theorem matrix.of_apply
added theorem matrix.of_sub_of
added theorem matrix.of_symm_apply
added theorem matrix.of_zero
added theorem matrix.smul_of
modified theorem matrix.cons_mul
modified theorem matrix.cons_val'
modified theorem matrix.cons_vec_mul
modified theorem matrix.head_transpose
modified theorem matrix.head_val'
modified theorem matrix.smul_mat_cons
modified theorem matrix.tail_transpose
modified theorem matrix.tail_val'
modified theorem matrix.transpose_empty_cols
modified theorem matrix.transpose_empty_rows
modified theorem matrix.vec_mul_cons
deleted theorem matrix.det_fin_two_mk
added theorem matrix.det_fin_two_of
modified theorem equiv.perm.coe_subsingleton
modified theorem algebra.trace_matrix_def