mathlib3

543ae52c - feat(analysis/normed_space/add_torsor): normed_add_torsor (#2814)

feat(analysis/normed_space/add_torsor): normed_add_torsor (#2814) Define the metric space structure on torsors of additive normed group actions. The motivating case is Euclidean affine spaces. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations for the discussion leading to this particular handling of the distance. Note: I'm not sure what the right way is to address the dangerous_instance linter error "The following arguments become metavariables. argument 1: (V : Type u_1)".