Commit 2022-01-08 15:04 b1955dca

View on Github →

feat(data/matrix/basic): infix notation for matrix.dot_product in locale matrix (#11289) I created an infix notation for matrix.dot_product in locale matrix. The notation was consulted with @eric-wieser in #11181.

Estimated changes

Modified src/data/matrix/basic.lean

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_diagonal

modified theorem matrix.dot_product_neg

modified theorem matrix.dot_product_single

modified theorem matrix.dot_product_star

modified theorem matrix.dot_product_sub

modified theorem matrix.dot_product_zero'

modified theorem matrix.dot_product_zero

modified theorem matrix.neg_dot_product

modified theorem matrix.single_dot_product

modified theorem matrix.star_dot_product

modified theorem matrix.star_dot_product_star

modified theorem matrix.sub_dot_product

modified theorem matrix.zero_dot_product'

modified theorem matrix.zero_dot_product