Commit 2024-02-07 05:43 deb48fab

View on Github →

chore: Matrix.mulVec and Matrix.vecMul get infix notation (#10297) Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20mul_vec.20and.20vec_mul

Estimated changes

modified theorem Matrix.linfty_opNorm_mulVec
modified theorem Matrix.mulVec_neg
modified theorem Matrix.mulVec_one
modified theorem Matrix.mulVec_transpose
modified theorem Matrix.mulVec_zero
modified theorem Matrix.neg_mulVec
modified theorem Matrix.neg_vecMul
modified theorem Matrix.one_mulVec
modified theorem Matrix.vecMul_neg
modified theorem Matrix.vecMul_one
modified theorem Matrix.vecMul_transpose
modified theorem Matrix.vecMul_zero
modified theorem Matrix.vec_one_mul
modified theorem Matrix.zero_mulVec
modified theorem Matrix.zero_vecMul
modified theorem Matrix.empty_mulVec
modified theorem Matrix.empty_vecMul
modified theorem Matrix.mulVec_empty
modified theorem Matrix.vecMul_empty
modified theorem Matrix.mulVec_cramer
modified theorem Matrix.toLin'_apply