feat: port LinearAlgebra.AffineSpace.Basic (#2165)

Mathlib.lean

@@ -742,6 +742,7 @@ import Mathlib.Lean.LocalContext
 import Mathlib.Lean.Message
 import Mathlib.Lean.Meta
 import Mathlib.Lean.Meta.Simp
+import Mathlib.LinearAlgebra.AffineSpace.Basic
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.Logic.Basic
 import Mathlib.Logic.Denumerable

Mathlib/LinearAlgebra/AffineSpace/Basic.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2020 Joseph Myers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Myers
+
+! This file was ported from Lean 3 source module linear_algebra.affine_space.basic
+! leanprover-community/mathlib commit 98e83c3d541c77cdb7da20d79611a780ff8e7d90
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.AddTorsor
+
+/-!
+# Affine space
+
+In this file we introduce the following notation:
+
+* `AffineSpace V P` is an alternative notation for `AddTorsor V P` introduced at the end of this
+  file.
+
+We tried to use an `abbreviation` instead of a `notation` but this led to hard-to-debug elaboration
+errors. So, we introduce a localized notation instead. When this notation is enabled with
+`open Affine`, Lean will use `AffineSpace` instead of `AddTorsor` both in input and in the
+proof state.
+
+Here is an incomplete list of notions related to affine spaces, all of them are defined in other
+files:
+
+* `AffineMap`: a map between affine spaces that preserves the affine structure;
+* `AffineEquiv`: an equivalence between affine spaces that preserves the affine structure;
+* `AffineSubspace`: a subset of an affine space closed w.r.t. affine combinations of points;
+* `AffineCombination`: an affine combination of points;
+* `AffineIndependent`: affine independent set of points;
+* `AffineBasis.coord`: the barycentric coordinate of a point.
+
+## TODO
+
+Some key definitions are not yet present.
+
+* Affine frames.  An affine frame might perhaps be represented as an `AffineEquiv` to a `Finsupp`
+  (in the general case) or function type (in the finite-dimensional case) that gives the
+  coordinates, with appropriate proofs of existence when `k` is a field.
+ -/
+
+
+scoped[Affine] notation "AffineSpace" => AddTorsor