Commit 2025-02-11 10:41 a4b60df9

chore(Data/ENNReal): restructure lemma files (#21649) This PR redoes the file structure in ENNReal in order to clean up (transitive) dependencies. Previously we had the import order Basic.lean -> Operations.lean -> Inv.lean -> Real.lean, and this PR updates it to follow Basic.lean -> Real.lean -> Order.lean -> Inv.lean -> Operations.lean. The motivation is that this order seems to follow the number of files that actually depend on declarations in each of these files. (See for example the import graph for metric spaces.) More specifically:

• Real.lean includes lemmas on toReal that can be proven without further assumptions. (This is the bulk of previous Real.lean.)
• Order.lean includes lemmas on monotonicity and operations applied to infinity. (This is the bulk of previous Operations.lean, and includes a bit of Real.lean.)
• Inv.lean includes lemmas on inverses and division. (This is the bulk of previous Inv.lean, and includes a bit of Real.lean.)
• Action.lean includes lemmas on scalar multiplication with NNReal. (This is mostly split off from Operations.lean.)
• Operations.lean includes lemmas on big operations such as finset sum and product. (This is the remainder of Operations.lean, and includes a bit of Real.lean.)