Commit 2025-07-15 17:23 845ff2b8

View on Github →

feat(Data/Matrix): add Matrix.vecCons_inj (#26896) vecCons_inj is the vecCons version of Fin.cons_inj. Also use it to simplify some proofs for vec2 and vec3. Zulip discussion

Estimated changes

Modified Mathlib/Data/Fin/VecNotation.lean

added theorem Matrix.vecCons_inj

Modified Mathlib/Data/Matrix/Notation.lean