Zulip Chat Archive Stream: mathlib4 Topic: Idiomatic approach to several distance metrics on same type Jackson Brough (Jul 22 2025 at 22:22): (deleted) Last updated: Feb 28 2026 at 14:05 UTC