Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes