mathlib3 documentation

linear_algebra.affine_space.basic

Affine space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_locale affine, Lean will use affine_space instead of add_torsor 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:

TODO #

Some key definitions are not yet present.