chore(linear_algebra/affine_space/basic): split (#4767)

* Split `linear_algebra/affine_space/basic` into two files: `affine_map` and `affine_subspace`.
* Move notation `affine_space` to the bottom of `algebra/add_torsor`.

src/algebra/add_torsor.lean

@@ -23,14 +23,17 @@ defines the notation `+ᵥ` for adding a group element to a point and
 
 ## Implementation notes
 
-Affine spaces are the motivating example of torsors of additive group
-actions.  It may be appropriate to refactor in terms of the general
-definition of group actions, via `to_additive`, when there is a use
-for multiplicative torsors (currently mathlib only develops the theory
-of group actions for multiplicative group actions).  The variable `G`
-is an explicit rather than implicit argument to lemmas because
-otherwise the elaborator sometimes has problems inferring appropriate
-types and type class instances.
+Affine spaces are the motivating example of torsors of additive group actions. It may be appropriate
+to refactor in terms of the general definition of group actions, via `to_additive`, when there is a
+use for multiplicative torsors (currently mathlib only develops the theory of group actions for
+multiplicative group actions).
+
+## Notations
+
+* `v +ᵥ p` is a notation for `has_vadd.vadd`, the left action of an additive monoid;
+
+* `p₁ -ᵥ p₂` is a notation for `has_vsub.vsub`, difference between two points in an additive torsor
+  as an element of the corresponding additive group;
 
 ## References
 

src/analysis/convex/basic.lean

@@ -6,7 +6,7 @@ Authors: Alexander Bentkamp, Yury Kudriashov
 import data.set.intervals.ord_connected
 import data.set.intervals.image_preimage
 import data.complex.module
-import linear_algebra.affine_space.basic
+import linear_algebra.affine_space.affine_map
 import algebra.module.ordered
 
 

src/analysis/normed_space/mazur_ulam.lean

@@ -6,7 +6,7 @@ Author: Yury Kudryashov
 import analysis.normed_space.point_reflection
 import topology.instances.real_vector_space
 import analysis.normed_space.add_torsor
-import linear_algebra.affine_space.basic
+import linear_algebra.affine_space.affine_map
 
 /-!
 # Mazur-Ulam Theorem

src/linear_algebra/affine_space/affine_equiv.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Yury G. Kudryashov
 -/
-import linear_algebra.affine_space.basic
+import linear_algebra.affine_space.affine_map
 
 /-!
 # Affine equivalences
@@ -28,6 +28,7 @@ affine space, affine equivalence
 -/
 
 open function set
+open_locale affine
 
 /-- An affine equivalence is an equivalence between affine spaces such that both forward
 and inverse maps are affine.