mathlib3

b542cfbc - chore(linear_algebra/basic): notation for span of a singleton (#5538)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/New.20linear.20algebra.20notation), [Zulip 2](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20span)