mathlib

6552f21e - feat(algebra/add_torsor): torsors of additive group actions (#2720)

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 https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations for the discussion leading to this particular structure.