Midpoint of a segment #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
Main theorems #
We do not mark most lemmas as
@[simp] because it is hard to tell which side is simpler.
midpoint x y is the midpoint of the segment
f : E → F sending zero to zero and midpoints to midpoints is an