# Commit 2022-09-28 06:21 494b1f8e

View on Github →feat(linear_algebra/affine_space/affine_subspace): `parallel`

(#16298)
Define the notion of two affine subspaces being parallel and set up
associated API.
This notion is very similar to the subspaces having equal `direction`

,
and in many cases I expect equality of direction will remain more
convenient to use. However, the notions aren't exactly the same (the
empty affine subspace and a single-point subspace have the same
`direction`

but aren't considered parallel), and having a definition
of `parallel`

, even if not used much, allows geometrical statements
involving things being parallel to be made in a way corresponding more
closely to the informal formulation.
Note that the notation defined for `parallel`

is based on what
characters are available rather than on their proper Unicode
semantics. There are at least four characters in Unicode with
somewhat similar appearance:

- U+01C1 LATIN LETTER LATERAL CLICK
`ǁ`

- U+2016 DOUBLE VERTICAL LINE
`‖`

(for which the Unicode Character Database says "used in pairs to indicate norm of a matrix") - U+2225 PARALLEL TO
`∥`

- U+23F8 DOUBLE VERTICAL BAR
`⏸`

Based on the Unicode descriptions, U+2225 would be natural to use for`parallel`

, and U+2016 for norms. However, mathlib makes extensive use of U+2225 for norms; for geometry, both norms and`parallel`

are of use and it doesn't work well to try to use the notation for both (unless there's some way to set the precedences of the different notations that will make Lean parse both uses correctly). (There's a local notation using U+2225 for`fuzzy`

in the context of games, which seems a more appropriate use of U+2225 and probably doesn't cause problems because of games and norms not being used together.) So this PR uses U+2016 for`parallel`

instead of the logical U+2225 (even if in principle the uses for`parallel`

and norms should be swapped to correspond better to the Unicode semantics). There are other local uses of U+2016 for`fintype.card`

in a few places, but I don't expect those to cause a problem.