Zulip Chat Archive

Stream: mathlib4

Topic: Valued.integer.properSpace_iff_completeSpace_and_isDiscreteV

Kenny Lau (Jul 25 2025 at 10:10):

Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField is 104 characters long (according to https://www.charactercountonline.com) and should be illegal

Ruben Van de Velde (Jul 25 2025 at 11:24):

Why?

Damiano Testa (Jul 25 2025 at 12:29):

You were not around when the number of characters of instance names did not fit in zulip messages. :laughing:

Last updated: Dec 20 2025 at 21:32 UTC