mathlib documentation


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_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:


Some key definitions are not yet present.