Theorem Matrix.empty_mulVec

Modification history

2024-02-07 05:43

Mathlib/Data/Matrix/Notation.lean

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

Modified Matrix.empty_mulVec View on Github →

2023-04-20 04:08

Mathlib/Data/Matrix/Notation.lean

feat: port Data.Matrix.Notation (#3427) …

Added Matrix.empty_mulVec View on Github →