Mathlib Changelog
v3
Changelog
About
Github
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
Created
src/algebra/midpoint.lean
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