Def LinearMap.vecCons

Modification history

2025-01-29 23:20

Mathlib/LinearAlgebra/Pi.lean

feat: `HasFDerivAt` for `Fin.cons` (#20407) …

Modified LinearMap.vecCons View on Github →

2023-02-14 06:34

Mathlib/LinearAlgebra/Pi.lean

feat: port LinearAlgebra.Pi (#2250)

Added LinearMap.vecCons View on Github →