Torsors of normed space actions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains lemmas about normed additive torsors over normed spaces.
A continuous map between two normed affine spaces is an affine map provided that
it sends midpoints to midpoints.