mathlib3

78261225 - chore(linear_algebra/affine_space/midpoint): factor out lemmas about char_zero (#18555)

chore(linear_algebra/affine_space/midpoint): factor out lemmas about char_zero (#18555) This removes the dependency on `char_p` in `analysis.convex.segment` and `analysis.normed.group.add_torsor`.