Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-05 04:42 d6ddfd2f

View on Github →

feat(algebra/midpoint): define midpoint, prove basic properties (#2599) Part of #2214

Estimated changes

added def midpoint
added theorem midpoint_add_add
added theorem midpoint_add_left
added theorem midpoint_add_right
added theorem midpoint_comm
added theorem midpoint_def
added theorem midpoint_eq_iff
added theorem midpoint_neg_neg
added theorem midpoint_self
added theorem midpoint_smul_smul
added theorem midpoint_sub_left
added theorem midpoint_sub_right
added theorem midpoint_sub_sub
added theorem midpoint_unique