Theorem Matrix.vecCons_inj

Modification history

2025-07-15 17:23
Mathlib/Data/Fin/VecNotation.lean
feat(Data/Matrix): add `Matrix.vecCons_inj` (#26896) …
Added Matrix.vecCons_injView on Github →