# 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.

An `AddTorsor G P`

gives a structure to the nonempty type `P`

,
acted on by an `AddGroup G`

with a transitive and free action given
by the `+ᵥ`

operation and a corresponding subtraction given by the
`-ᵥ`

operation. In the case of a vector space, it is an affine
space.

## Equations

- Affine.termAffineSpace = Lean.ParserDescr.node `Affine.termAffineSpace 1024 (Lean.ParserDescr.symbol "AffineSpace")