Commit 2025-06-06 00:15 114334c0

style: ++ notation for List.Vector (#25487) In Mathlib 3, the ++ notation was homogeneous so couldn't be used for List.Vector.append : List.Vector α n → List.Vector α m → List.Vector α (n + m). Now we can use this ++ notation, as _root_.Vector use it.