basic): norm lemmas for lipschitz and antilipschitz (#19103)

Commit

2 years ago

feat(analysis/normed/group/basic): norm lemmas for lipschitz and antilipschitz (#19103) This also corrects some nonsense names produced by to_additive.

Author

eric-wieser

Parents

d3b54a9f

mathlib 41bef4ae - feat(analysis/normed/group/basic): norm lemmas for lipschitz and antilipschitz (#19103)

mathlib
41bef4ae - feat(analysis/normed/group/basic): norm lemmas for lipschitz and antilipschitz (#19103)