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.
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.