Zulip Chat Archive

Stream: mathlib4

Topic: WithTop.LinearOrderedAddCommGroup.coe_neg

Ruben Van de Velde (May 14 2025 at 20:43):

Is docs#WithTop.LinearOrderedAddCommGroup.coe_neg really the right name?

Eric Wieser (May 14 2025 at 21:11):

I think namespace should be section in that file

Last updated: Dec 20 2025 at 21:32 UTC