Commit 2024-10-22 10:52 fb1cb210

View on Github →

chore(Analysis/SpecificLimits/Normed): move lemmas earlier (#18046) These lemmas can be proved earlier at no cost. This is one step towards reducing imports in this area of mathlib.

Estimated changes