notation}): `cons_{add,sub,dot_product}_cons` (#11241)

Commit

4 years ago

feat(data/{fin/vec_notation, matrix/notation}): `cons_{add,sub,dot_product}_cons` (#11241) While these can be proved by `simp`, they are not rejected by the simp linter.

Author

eric-wieser

Parents

98b64f49

mathlib3 b27e33a0 - feat(data/{fin/vec_notation, matrix/notation}): `cons_{add,sub,dot_product}_cons` (#11241)

mathlib3
b27e33a0 - feat(data/{fin/vec_notation, matrix/notation}): `cons_{add,sub,dot_product}_cons` (#11241)