Def Matrix.vecAppend

Modification history

2023-08-10 19:52

Mathlib/Data/Fin/VecNotation.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Matrix.vecAppend View on Github →

2023-01-23 16:46

Mathlib/Data/Fin/VecNotation.lean

feat: port Data.Fin.VecNotation (#1741)

Added Matrix.vecAppend View on Github →