IMPORTANT NOTATION CHANGE

Stream: Equational

[Terence Tao]

We have just pushed a notation change to make the magma operation ◇ (\diw) instead of ◦︎ (\circ), both in the Lean code and in the blueprint. This may create various merge conflicts in all current PRs - apologies in advance for the inconvenience caused. The rationale for this is that by deconflicting the magma operation with function composition, considerably faster Lean compile times have been observed. The symbol ◇ was chosen to have a short macro \diw, to not be in global use by Mathlib, and to be somewhat visually similar to ◦︎. More discussion at https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Symbol.20for.20.60Magma.2Eop.60

Ideally, other components of the project (e.g., the experimental equation graph explorer at https://nicholas.carlini.com/tmp/view.html ) should change over to this new notation also, but this is not urgent. Legacy code and files can also be converted over, but again this should be low priority except for regularly scheduled automated code runs.