Commit 2025-04-14 12:29 ece17b30

View on Github →

feat: add a dsimproc for vector notation (#13578) Zulip

Estimated changes

Modified Archive/Imo/Imo2024Q5.lean

Modified Mathlib/Algebra/Order/Antidiag/Nat.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/Data/Fin/VecNotation.lean

modified theorem Matrix.cons_val_one

modified theorem Matrix.cons_val_two

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

Modified Mathlib/LinearAlgebra/CrossProduct.lean

Modified Mathlib/LinearAlgebra/Projectivization/Independence.lean

Modified Mathlib/LinearAlgebra/Ray.lean

Modified Mathlib/RingTheory/Complex.lean

Modified MathlibTest/matrix.lean

Modified MathlibTest/vec_notation.lean