Commit 2022-09-28 06:21 494b1f8e

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.