Abbreviation for ∙?

Stream: general

[Yury G. Kudryashov]

Should we add an abbreviation for ∙ as in K ∙ v = Submodule.span K {v}?

[Yury G. Kudryashov]

Question to those who use this notation: what local abbreviation did you add for this symbol?

[Yury G. Kudryashov]

In Lean 3 it was available as \. but now it is taken by · MIDDLE DOT

[Yury G. Kudryashov]

@Heather Macbeth :up:

[Heather Macbeth]

Funny, I can't remember! Don't we have a big table of VS Code shortcuts somewhere, though?

[Yury G. Kudryashov]

https://raw.githubusercontent.com/leanprover/vscode-lean4/master/vscode-lean4/src/abbreviation/abbreviations.json

[Yury G. Kudryashov]

The problem is that \. is now taken for the "focus on the first goal" / "placeholder for a lambda function" symbol.

[Yury G. Kudryashov]

So, what should be the new shortcut?

[Kevin Buzzard]

Is cdot used? That's what I type in latex

[Yury G. Kudryashov]

It is used for ⬝ (matrix multiplication)

[Johan Commelin]

I suppose we can now use * for matrix multiplication in ml4, right?

[Johan Commelin]

Because of HMul.

[Patrick Massot]

Heather Macbeth said:

Funny, I can't remember! Don't we have a big table of VS Code shortcuts somewhere, though?

In the VSCode extension you can access that table using Ctrl-shift-p Lean4: Show all abbreviations

[Yury G. Kudryashov]

@Johan Commelin Will Lean try to cast both sides to the same type?

[Johan Commelin]

No, I think we can teach it that (m x n)-matrix times (n x o) matrix is of size (m x o)

[Eric Wieser]

Should we change the notation to reuse • now?

[Eric Wieser]

instance : HSMul (Type u) M where hSMul R x := span R x

[Johan Commelin]

That doesn't type check, right?

[Johan Commelin]

span R x only makes sense if there is a semiring instance for R

[Johan Commelin]

And a Module R M instance

[Eric Wieser]

Oh, good point

[Eric Wieser]

Maybe we can still overload the notation in the elaborator