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.

Estimated changes

modified theorem cross_anticomm'
modified theorem cross_anticomm
modified theorem cross_cross
modified theorem cross_self
modified theorem dot_cross_self
modified theorem dot_self_cross
modified theorem jacobi_cross
modified theorem leibniz_cross
modified theorem triple_product_eq_det
modified theorem triple_product_permutation