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: Dec 20 2025 at 21:32 UTC