mathlib

0b9afe18 - chore(linear_algebra/affine_space): redefine `line_map`, add `to_affine_subspace` (#4643)

chore(linear_algebra/affine_space): redefine `line_map`, add `to_affine_subspace` (#4643) * now `line_map` takes two points on the line, not a point and a direction, update/review lemmas; * add `submodule.to_affine_subspace`; * add `affine_map.fst` and `affine_map.snd`; * prove that an affine map `ℝ → ℝ` sends an unordered interval to an unordered interval.