Def PiFin.mkLiteralQ

Modification history

2025-11-19 06:07
Mathlib/Data/Fin/VecNotation.lean
chore: move Mathlib to the module system (#31786) …
Deleted PiFin.mkLiteralQView on Github →
2025-04-17 23:56
Mathlib/Data/Fin/VecNotation.lean
feat: `PiFin.mkLiteralQ` and `Matrix.mkLiteralQ` (#24101) …
Added PiFin.mkLiteralQView on Github →