The divergence of a curl vanishes: $\nabla\cdot(\nabla\times F)=0$

Proved

ContinuityEqWiki.div_curl_eq_zero

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

continuity-equationmathematical-physics

Let $F:\mathbb R^3\to\mathbb R^3$ be a vector field of class $C^2$ . Then for every $x\in\mathbb R^3$ ,

\nabla\cdot(\nabla\times F)(x)=0.

The source uses this identity when it takes the divergence of Ampère's law to derive charge conservation from Maxwell's equations.

Preamble

import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs

Formal statement

namespace ContinuityEqWiki

theorem div_curl_eq_zero (F : Space → Space) (hF : ContDiff ℝ 2 F) (x : Space) :
    div (curl F) x = 0 := by sorry

end ContinuityEqWiki

Source

Wikipedia, "Continuity equation", revision oldid=1378634825, https://en.wikipedia.org/w/index.php?title=Continuity_equation&oldid=1378634825, section "Electromagnetism", box "Consistency with Maxwell's equations" ("but the divergence of a curl is zero")

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - drafting agent, non-blind read-back

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, at the explicit request of the proposal owner. Its author knew the source text and the intended meaning while writing it, so it must not be mistaken for a blind, independent audit. Reviewers should compare the Lean code against the source themselves.

For every $F:\mathbb R^3\to\mathbb R^3$ that is $C^2$ on all of $\mathbb R^3$ and every point $x\in\mathbb R^3$ ,

\sum_{i=0}^{2}\partial_i\big((\nabla\times F)_i\big)(x)=0,

where $\nabla\times F=(\partial_1F_2-\partial_2F_1,\ \partial_2F_0-\partial_0F_2,\ \partial_0F_1-\partial_1F_0)$ and each $\partial_i$ is the Fréchet derivative applied to the $i$ -th unit vector.

View graph

The divergence of a curl vanishes: ∇⋅(∇×F)=0\nabla\cdot(\nabla\times F)=0∇⋅(∇×F)=0

The divergence of a curl vanishes: $\nabla\cdot(\nabla\times F)=0$