Derivative of the inverse metric

Let $g_{\alpha\beta}(x)$ be a smooth, symmetric, nondegenerate metric on a coordinate chart $\mathbb R^n$, with inverse $g^{\alpha\beta}(x)$. Then for all indices $\alpha,\beta,\gamma$ and every point $x$,

with summation over $\delta,\epsilon$. It follows from differentiating $g^{\beta\delta}g_{\delta\gamma}=\delta^\beta_\gamma$.

This identity is used throughout the note to trade derivatives of the inverse metric for derivatives of the metric.

Formalization Note Space-time is a single global chart $\mathbb R^n$ (Fin n → ℝ); $\partial_\alpha$ is the Fréchet derivative in direction $e_\alpha$; the metric is assumed smooth, symmetric and pointwise invertible (IsSmoothMetric), with no signature condition.