Zulip Chat Archive
Stream: triage
Topic: PR !4#29933: chore: fix `def` naming isses in `Normed/Fie...
Random Issue Bot (Jan 10 2026 at 14:11):
Today I chose PR #29933 for discussion!
chore: fix def naming isses in Normed/Field/WithAbs.lean
Created by @Salvatore Mercuri (@smmercuri) on 2025-09-24
Labels: WIP, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Ruben Van de Velde (Jan 10 2026 at 18:56):
Seems still relevant
Last updated: Feb 28 2026 at 14:05 UTC