Def EuclideanSpace.delabVecNotation

Modification history

2025-11-19 06:07
Mathlib/Analysis/InnerProductSpace/PiL2.lean
chore: move Mathlib to the module system (#31786) …
Deleted EuclideanSpace.delabVecNotationView on Github →
2024-12-02 17:27
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat: notation for vectors in Euclidean space (#17732) …
Added EuclideanSpace.delabVecNotationView on Github →