Commit 2024-12-02 17:27 c4651942

feat: notation for vectors in Euclidean space (#17732) This adds !₂[1, 2, 3] notation for (WithLp.equiv 2 (∀ _ : Fin 3, _)).symm ![1, 2, 3], which is a term of type EuclideanSpace 𝕜 (Fin 3); and more generally for other Lp norms, using the subscript parser. This reduces the temptation to write the type-incorrect ![1, 2, 3] that has the wrong norm. The (parser for the) subscript parser relies on initializers running, and so a missing Lean.enableInitializersExecution has to be inserted in checkYaml.lean. It has already been inserted in the necessary places in upstream repos. Notation Zulip poll.