Commit 2025-12-21 14:55 c3d2e6f2
View on Github →chore(Analysis/Meromorphic/Basic): remove redundant fun_ lemmas (#33144)
This PR removes some lemmas fun_deriv and fun_iterated_deriv, because they are purely eta-expanded forms of existing lemmas. There is no scenario where these lemmas would be more useful than the existing lemmas.
Since the lemmas are very new, they don't need a deprecation.