mathlib3

beee53c9 - feat(linear_algebra/affine_space/affine_subspace): notation for lines (#17094)

feat(linear_algebra/affine_space/affine_subspace): notation for lines (#17094) In informal geometry, the line through two points A and B might be referred to as "line AB" or just "AB". In mathlib, we currently have to use the more cumbersome `affine_span ℝ ({A, B} : set P)` (in most places the elaborator needs that explicit `: set P` annotation). Add notation that allows `line[ℝ, A, B]`, closer to informal usage, to be used instead (we already have notation for the `submodule.span` of a single vector; affine spans of two points are generally analogous to linear spans of one vector). The definition of the notation names the `set.has_singleton` instance explicitly, so avoiding the need to pass the type of points as an argument to the notation. (Unfortunately, the pretty-printer won't use the notation when displaying goal state, which I think is a general issue with such notation defined using `@`.)