Def Matrix.mkLiteralQ

Modification history

2025-11-19 06:07

Mathlib/LinearAlgebra/Matrix/Notation.lean

chore: move Mathlib to the module system (#31786) …

Deleted Matrix.mkLiteralQ View on Github →

2025-04-17 23:56

Mathlib/Data/Matrix/Notation.lean

feat: `PiFin.mkLiteralQ` and `Matrix.mkLiteralQ` (#24101) …

Added Matrix.mkLiteralQ View on Github →