Zulip Chat Archive
Stream: mathlib4
Topic: Mathlib/Data/ENNReal
Michael Rothgang (Apr 16 2025 at 07:43):
Thinking about the contents of the data directory: should Data/ENNReal move elsewhere? To Analysis maybe, or to MeasureTheory?
Michael Rothgang (Apr 16 2025 at 07:45):
Or is Data meant for exactly that?
Ruben Van de Velde (Apr 16 2025 at 08:14):
Probably if Real stays in Data, so should ENNReal
Ruben Van de Velde (Apr 16 2025 at 08:16):
(Vaguely relatedly, I have an unfinished branch#nnreal-archimedean to see if making Data.ENNReal.Defs lighter is useful)
Last updated: May 02 2025 at 03:31 UTC