Differentiating the determinant entry by entry

Proved

DifferentialGeometry.Integral.Measure.hasDerivAt_det_of_entries

by Xinze-Li-Moqian · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

closed-surface-area-variationcolding-minicozziricci-flowriemannian-geometry

Let $G(s)$ be a real square matrix family on a finite index type, with entry derivatives $G'_{ij}$ at $t$ . Then

\frac{d}{dt}\det G(t)=\sum_\sigma\operatorname{sgn}(\sigma)\sum_kG'_{\sigma(k),k}\prod_{i\ne k}G_{\sigma(i),i}(t).

No invertibility assumption is required. The proof differentiates the finite Leibniz expansion.

Proof from DifferentialGeometry, preserved and packaged by OpenGA with source attribution.

Preamble

import Definitions.Def_OpenGA_ImmersedMetric
import Mathlib.Analysis.Calculus.Deriv.Add
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.LinearAlgebra.Matrix.Adjugate
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.Trace

noncomputable section

open Matrix

open scoped Matrix BigOperators

namespace DifferentialGeometry
end DifferentialGeometry
open _root_.DifferentialGeometry

namespace DifferentialGeometry.Integral
end DifferentialGeometry.Integral
open _root_.DifferentialGeometry
open _root_.DifferentialGeometry.Integral

namespace DifferentialGeometry.Integral.Measure
end DifferentialGeometry.Integral.Measure
open _root_.DifferentialGeometry
open _root_.DifferentialGeometry.Integral
open _root_.DifferentialGeometry.Integral.Measure

variable {n : Type*} [Fintype n] [DecidableEq n]

namespace DifferentialGeometry.Integral.Measure
end DifferentialGeometry.Integral.Measure
open _root_.DifferentialGeometry.Integral.Measure

Formal statement

theorem DifferentialGeometry.Integral.Measure.hasDerivAt_det_of_entries
    (G : ℝ → Matrix n n ℝ) (G' : Matrix n n ℝ) (t : ℝ)
    (hG : ∀ i j, HasDerivAt (fun t => G t i j) (G' i j) t) :
    HasDerivAt (fun t => (G t).det)
      (∑ σ : Equiv.Perm n, ((Equiv.Perm.sign σ : ℤ) : ℝ) *
        ∑ k, (∏ i ∈ Finset.univ.erase k, G t (σ i) i) * G' (σ k) k) t := by sorry

Source

https://github.com/qinz1yang/differential-geometry/blob/1b535dd102b94cc42b107cca27059687888f08b3/DifferentialGeometry/Analysis/Integration/Measure/JacobiFormula.lean#L34-L65

View graph