Commit 2025-11-26 21:08 feb1bf6e

feat: $C^n$ implicit function theorem (#30595) I formalise a proof that the implicit function obtained from a $C^n$ implicit equation ($n \geq 1$) is $C^n$. Roughly speaking, given an equation $f : E \times F \to F$ that is smooth at $(a,b) : E\times F$ and whose derivative $f'$ is in some sense non-singular, then there exists a function $\phi : E \to F$ such that $\phi(a) = b$, $f(x, \phi(x)) = f(a,b)$ for all $x$ in a neighbourhood of $a$, and $\phi$ is $C^n$ at $a$. The current implicit function theorem in Mathlib is quite general and not directly applicable to many familiar scenarios. The statements added by this PR correspond to, e.g., the way the theorem is described on Wikipedia, and will be directly useful for an upcoming formalisation of the smoothness theorem for flows of ODEs.

• depends on: #30607