Commit 2021-01-01 19:02 b542cfbc

chore(linear_algebra/basic): notation for span of a singleton (#5538) Notation ∙ (\.) for the span of a single element of a module, so one can write R ∙ x instead of span R {x}. This in itself does not save so many keystrokes, but it also seems to be a bit more robust: it works in settings where previously one had to type span R ({x} : set M) because the type of the singleton was not recognised. Zulip 1, Zulip 2