Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-16 00:27 4ae97924

View on Github →

chore(data/matrix/basic): add lemmas about dot_product and mul_vec (#8325) This renames:

  • mul_vec_one to one_mul_vec
  • mul_vec_zero to zero_mul_vec and adds the new lemmas:
  • sub_mul_vec
  • mul_vec_sub
  • zero_mul_vec
  • mul_vec_zero
  • sub_dot_product
  • dot_product_sub Some existing lemmas have had their variables extracted to sections.

Estimated changes

modified theorem matrix.add_dot_product
modified theorem matrix.diagonal_dot_product
modified theorem matrix.dot_product_add
modified theorem matrix.dot_product_diagonal
modified theorem matrix.dot_product_neg
modified theorem matrix.dot_product_smul
modified theorem matrix.dot_product_star
added theorem matrix.dot_product_sub
modified theorem matrix.dot_product_zero'
modified theorem matrix.dot_product_zero
deleted theorem matrix.mul_vec_one
modified theorem matrix.neg_dot_product
added theorem matrix.one_mul_vec
modified theorem matrix.smul_dot_product
modified theorem matrix.star_dot_product
added theorem matrix.sub_dot_product
modified theorem matrix.vec_mul_zero
modified theorem matrix.zero_dot_product'
modified theorem matrix.zero_dot_product
added theorem matrix.zero_mul_vec
added theorem matrix.zero_vec_mul