Rename `times` to `cross`

Pro:

• Easier to discover (at least in my experience), esp. if you already know that dot refers to a multiplication dot, then I'd expect to find the multiplication cross under the according name.
• Nicely parallels the naming between cross and dot product.
• times could mean any kind of multiplication symbol; cross is more descriptive (esp. considering differing conventions, like in Germany, where the typical "times" symbol is almost always a dot).

Con:

• Precedent of HTML using ×, LaTeX using \times, and codepoints like U+2297 CIRCLED TIMES in Unicode.
• Might be assumed to refer to crossmark or similar.
• Obviously quite breaking.

Concerning the last point, an alternative could be to support both names, similar to infinity and oo coexisting. I'm unaware if this proposal has been discussed and/or declined in the past.

The issue proposes renaming times to cross, while also raising support for both names as an alternative. No files, tests, or entry points are identified; first review the six-comment discussion and locate the existing times, infinity, and oo symbol definitions and references. Done requires an agreed naming direction and consistent handling of the affected symbols.