Zulip Chat Archive
Stream: mathlib4
Topic: Is there a definition of vector norm in the mathlib library?
qutrit (Feb 14 2025 at 02:36):
It is the sum of the squares of the magnitudes of all elements in the vector.
Yury G. Kudryashov (Feb 14 2025 at 03:51):
Yaël Dillies (Feb 14 2025 at 08:03):
Do you know about docs#EuclideanSpace ?
Last updated: May 02 2025 at 03:31 UTC