Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-07 05:17 7d240ce1

View on Github →

chore(data/matrix/notation): split into 2 files (#10199) I want to use ![a, b] notation in some files that don't need to import data.matrix.basic.

Estimated changes

added theorem matrix.add_cons
added theorem matrix.cons_add
added theorem matrix.cons_append
added theorem matrix.cons_fin_one
added theorem matrix.cons_head_tail
added theorem matrix.cons_sub
added theorem matrix.cons_val_one
added theorem matrix.cons_val_succ'
added theorem matrix.cons_val_succ
added theorem matrix.cons_val_zero'
added theorem matrix.cons_val_zero
added theorem matrix.cons_vec_alt0
added theorem matrix.cons_vec_alt1
added theorem matrix.cons_zero_zero
added theorem matrix.empty_add_empty
added theorem matrix.empty_append
added theorem matrix.empty_eq
added theorem matrix.empty_sub_empty
added theorem matrix.empty_val'
added theorem matrix.empty_vec_alt0
added theorem matrix.empty_vec_alt1
added theorem matrix.head_add
added theorem matrix.head_cons
added theorem matrix.head_fin_const
added theorem matrix.head_neg
added theorem matrix.head_sub
added theorem matrix.head_zero
added theorem matrix.neg_cons
added theorem matrix.neg_empty
added theorem matrix.range_cons
added theorem matrix.range_empty
added theorem matrix.smul_cons
added theorem matrix.smul_empty
added theorem matrix.sub_cons
added theorem matrix.tail_add
added theorem matrix.tail_cons
added theorem matrix.tail_neg
added theorem matrix.tail_sub
added theorem matrix.tail_zero
added def matrix.vec_alt0
added theorem matrix.vec_alt0_append
added def matrix.vec_alt1
added theorem matrix.vec_alt1_append
added def matrix.vec_cons
added theorem matrix.vec_cons_const
added def matrix.vec_empty
added def matrix.vec_head
added def matrix.vec_tail
added theorem matrix.zero_empty
deleted theorem matrix.add_cons
deleted theorem matrix.cons_add
deleted theorem matrix.cons_append
deleted theorem matrix.cons_eq_zero_iff
deleted theorem matrix.cons_fin_one
deleted theorem matrix.cons_head_tail
deleted theorem matrix.cons_nonzero_iff
deleted theorem matrix.cons_sub
deleted theorem matrix.cons_val_fin_one
deleted theorem matrix.cons_val_one
deleted theorem matrix.cons_val_succ'
deleted theorem matrix.cons_val_succ
deleted theorem matrix.cons_val_zero'
deleted theorem matrix.cons_val_zero
deleted theorem matrix.cons_vec_alt0
deleted theorem matrix.cons_vec_alt1
deleted theorem matrix.cons_zero_zero
deleted theorem matrix.empty_add_empty
deleted theorem matrix.empty_append
deleted theorem matrix.empty_eq
deleted theorem matrix.empty_sub_empty
deleted theorem matrix.empty_val'
deleted theorem matrix.empty_vec_alt0
deleted theorem matrix.empty_vec_alt1
deleted theorem matrix.head_add
deleted theorem matrix.head_cons
deleted theorem matrix.head_fin_const
deleted theorem matrix.head_neg
deleted theorem matrix.head_sub
deleted theorem matrix.head_zero
deleted theorem matrix.neg_cons
deleted theorem matrix.neg_empty
deleted theorem matrix.range_cons
deleted theorem matrix.range_empty
deleted theorem matrix.smul_cons
deleted theorem matrix.smul_empty
deleted theorem matrix.sub_cons
deleted theorem matrix.tail_add
deleted theorem matrix.tail_cons
deleted theorem matrix.tail_neg
deleted theorem matrix.tail_sub
deleted theorem matrix.tail_zero
deleted def matrix.vec_alt0
deleted theorem matrix.vec_alt0_append
deleted def matrix.vec_alt1
deleted theorem matrix.vec_alt1_append
deleted def matrix.vec_cons
deleted theorem matrix.vec_cons_const
deleted def matrix.vec_empty
deleted def matrix.vec_head
deleted theorem matrix.vec_head_vec_alt0
deleted theorem matrix.vec_head_vec_alt1
deleted def matrix.vec_tail
deleted theorem matrix.zero_empty