Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 06:18 67c2b5a0

View on Github →

feat(analysis/normed_space/add_torsor): distance to midpoint (#4849)

Estimated changes

added theorem dist_center_homothety
added theorem dist_homothety_center
added theorem dist_homothety_self
added theorem dist_left_midpoint
added theorem dist_midpoint_left
added theorem dist_midpoint_right
added theorem dist_right_midpoint
added theorem dist_self_homothety
added theorem dist_vadd_left
added theorem dist_vadd_right