Commit 2025-08-19 22:25 0b78b878
View on Github →refactor: crossProduct notation (#27006)
Replace ×₃
with ⨯₃
(\X
or \crossproduct
), and manually deprecate the old syntax.
See #mathlib4 > Notation for crossProduct
The deprecated notation used U+00D7 (https://util.unicode.org/UnicodeJsps/character.jsp?a=00D7) which is designated for multiplication in general while the updated notation using U+2A2F (https://util.unicode.org/UnicodeJsps/character.jsp?a=2A2F) is reserved specifically for the cross product.