basic): `dist (a * b) b` (#17240)

Commit

3 years ago

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

Author

YaelDillies

Parents