Commit 2024-10-22 16:44 93c444d3
View on Github →chore(Data/ENNReal): split off Lemmas file (#17919)
Almost all of Data.ENNReal.Basic can be done with much a smaller set of imports. We only have two lemmas that need more imports, so let's split them off to a new file.