Commit 2021-01-01 19:02 b542cfbc
View on Github →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