Commit 2023-03-24 13:33 5ceaff97

View on Github →

feat: port LinearAlgebra.AffineSpace.Midpoint (#2866) Added two new lemmas to make the simpNF linter happy.

Estimated changes

added theorem AffineMap.map_midpoint
added theorem left_eq_midpoint_iff
added theorem left_sub_midpoint
added theorem left_vsub_midpoint
added def midpoint
added theorem midpoint_add_self
added theorem midpoint_add_sub
added theorem midpoint_comm
added theorem midpoint_eq_iff'
added theorem midpoint_eq_iff
added theorem midpoint_eq_left_iff
added theorem midpoint_eq_right_iff
added theorem midpoint_eq_smul_add
added theorem midpoint_neg_self
added theorem midpoint_self
added theorem midpoint_self_neg
added theorem midpoint_sub_add
added theorem midpoint_sub_left
added theorem midpoint_sub_right
added theorem midpoint_unique
added theorem midpoint_vadd_midpoint
added theorem midpoint_vsub
added theorem midpoint_vsub_left
added theorem midpoint_vsub_midpoint
added theorem midpoint_vsub_right
added theorem midpoint_zero_add
added theorem right_eq_midpoint_iff
added theorem right_sub_midpoint
added theorem right_vsub_midpoint
added theorem vsub_midpoint