Affine space #

In this file we introduce the following notation:

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:


Some key definitions are not yet present.

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.

Instances For