Theorem Matrix.vec_one_mul

Modification history

2024-02-07 05:43

Mathlib/Data/Matrix/Basic.lean

chore: `Matrix.mulVec` and `Matrix.vecMul` get infix notation (#10297) …

Modified Matrix.vec_one_mul View on Github →

2023-04-24 00:27

Mathlib/Data/Matrix/Basic.lean

feat: Miscellaneous defs and lemmas (#3589) …

Added Matrix.vec_one_mul View on Github →