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