Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-25 06:35 6552f21e

View on Github →

feat(algebra/add_torsor): torsors of additive group actions (#2720) Define torsors of additive group actions, to the extent needed for (and with notation motivated by) affine spaces, to the extent needed for Euclidean spaces. See for the discussion leading to this particular structure.

Estimated changes