Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 03:23 4a681f15

View on Github →

feat(analysis/normed/group/basic): dist (a * b) b (#17240) dist (a * b) b = ∥a∥

Estimated changes

added theorem dist_mul_self_left
added theorem dist_mul_self_right