LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Divergence and curl are linear and satisfy the scalar product rules

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, let $F, G : U \to R^{n}$ be $C^{1}$ , let $f : U \to R$ be $C^{1}$ and let $a, b \in R$ . Then $a F + b G$ and $f F$ are $C^{1}$ on $U$ and

$div (a F + b G) = a div F + b div G,$

$div (f F) = ⟨ \nabla f, F ⟩ + f div F .$

If moreover $n = 3$ , then

$curl (a F + b G) = a curl F + b curl G, curl (f F) = \nabla f \times F + f curl F .$

Here $div$ , $curl$ and the coordinate naming are those of Divergence and curl of a $C^{1}$ vector field, $\nabla f$ is the gradient of The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, $⟨ \cdot, \cdot ⟩$ is the inner product of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\times$ is the cross product of The cross product in $R^{3}$ .

Facts & Assumptions

Given: The open set $U$ , the $C^{1}$ maps $F, G : U \to R^{n}$ , the $C^{1}$ scalar $f : U \to R$ and the reals $a, b$ of the Statement.

[F1]

The divergence of a $C^{1}$ field $F$ on an open $U \subseteq R^{n}$ is $div F = \sum_{i < n} \partial_{i} F_{i}$ , and for $n = 3$ its curl is $curl F = (\partial_{y} F_{z} - \partial_{z} F_{y}, \partial_{z} F_{x} - \partial_{x} F_{z}, \partial_{x} F_{y} - \partial_{y} F_{x})$ (Divergence and curl of a $C^{1}$ vector field).

[F2]

For scalar-valued $f$ on an open subset of $R^{m}$ , the gradient is $\nabla f = (\partial_{0} f, \dots, \partial_{m - 1} f)$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[F3]

For $u = (u_{x}, u_{y}, u_{z})$ and $v = (v_{x}, v_{y}, v_{z})$ in $R^{3}$ , $u \times v = (u_{y} v_{z} - u_{z} v_{y}, u_{z} v_{x} - u_{x} v_{z}, u_{x} v_{y} - u_{y} v_{x})$ (The cross product in $R^{3}$ ).

[F4]

For $x, y \in R^{m}$ , $⟨ x, y ⟩ = \sum_{k < m} x_{k} y_{k}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F5]

A map $f : U \to R^{q}$ is of class $C^{k}$ when each component is of class $C^{k}$ ( $C^{k}$ Euclidean maps and diffeomorphisms).

[L1]

For real functions of one real variable differentiable at a point, $f + g$ is differentiable there with $(f + g)^{'} = f^{'} + g^{'}$ , $α f$ is differentiable there with $(α f)^{'} = α f^{'}$ , and $f g$ is differentiable there with $(f g)^{'} = f^{'} g + f g^{'}$ (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

Proof

technique · direct

1.1givenL1F5

A partial derivative $\partial_{j}$ at a point $p$ is the ordinary one-variable derivative at $0$ of $t \mapsto (\cdot) (p + t e_{j})$ , so [L1] applies to it verbatim: for scalar $C^{1}$ functions $u, v$ on $U$ and reals $a, b$ one has $\partial_{j} (a u + b v) = a \partial_{j} u + b \partial_{j} v$ and $\partial_{j} (u v) = (\partial_{j} u) v + u \partial_{j} v$ pointwise on $U$ , and the right-hand sides are continuous, so $a u + b v$ and $u v$ are again $C^{1}$ .

1.2givenL1F5

Applying 1.1 componentwise, $a F + b G$ and $f F$ have $C^{1}$ components, hence are $C^{1}$ by [F5]; so all four expressions in the Statement are defined.

2.1step 1.1F1algebra

By [F1], $div (a F + b G) = \sum_{i < n} \partial_{i} (a F_{i} + b G_{i})$ , and step 1.1 rewrites each summand as $a \partial_{i} F_{i} + b \partial_{i} G_{i}$ ; summing gives $a \sum_{i < n} \partial_{i} F_{i} + b \sum_{i < n} \partial_{i} G_{i} = a div F + b div G$ .

2.2step 1.1F1algebra

By [F1], the first coordinate of $curl (a F + b G)$ is $\partial_{y} (a F_{z} + b G_{z}) - \partial_{z} (a F_{y} + b G_{y})$ , which step 1.1 rewrites as $a (\partial_{y} F_{z} - \partial_{z} F_{y}) + b (\partial_{y} G_{z} - \partial_{z} G_{y})$ ; the second coordinate is $\partial_{z} (a F_{x} + b G_{x}) - \partial_{x} (a F_{z} + b G_{z}) = a (\partial_{z} F_{x} - \partial_{x} F_{z}) + b (\partial_{z} G_{x} - \partial_{x} G_{z})$ and the third is $\partial_{x} (a F_{y} + b G_{y}) - \partial_{y} (a F_{x} + b G_{x}) = a (\partial_{x} F_{y} - \partial_{y} F_{x}) + b (\partial_{x} G_{y} - \partial_{y} G_{x})$ . The three coordinates are those of $a curl F + b curl G$ .

2.3step 1.1F1F2F4algebra

By [F1], $div (f F) = \sum_{i < n} \partial_{i} (f F_{i})$ , and step 1.1 rewrites each summand as $(\partial_{i} f) F_{i} + f \partial_{i} F_{i}$ . Splitting the sum gives $\sum_{i < n} (\partial_{i} f) F_{i} + f \sum_{i < n} \partial_{i} F_{i}$ , whose first term is $⟨ \nabla f, F ⟩$ by [F2] and [F4] and whose second is $f div F$ by [F1].

2.4step 1.1F1F2F3algebra

By [F1], the first coordinate of $curl (f F)$ is $\partial_{y} (f F_{z}) - \partial_{z} (f F_{y})$ , which step 1.1 rewrites as $((\partial_{y} f) F_{z} - (\partial_{z} f) F_{y}) + f (\partial_{y} F_{z} - \partial_{z} F_{y})$ . By [F2] and [F3] with $u = \nabla f$ and $v = F$ , the first bracket is the first coordinate $u_{y} v_{z} - u_{z} v_{y}$ of $\nabla f \times F$ , and the second summand is $f$ times the first coordinate of $curl F$ .

2.5step 1.1F1F2F3algebra

By [F1], the second coordinate of $curl (f F)$ is $\partial_{z} (f F_{x}) - \partial_{x} (f F_{z})$ , which step 1.1 rewrites as $((\partial_{z} f) F_{x} - (\partial_{x} f) F_{z}) + f (\partial_{z} F_{x} - \partial_{x} F_{z})$ . By [F2] and [F3] the first bracket is the second coordinate $u_{z} v_{x} - u_{x} v_{z}$ of $\nabla f \times F$ , and the second summand is $f$ times the second coordinate of $curl F$ .

2.6step 1.1F1F2F3algebra

By [F1], the third coordinate of $curl (f F)$ is $\partial_{x} (f F_{y}) - \partial_{y} (f F_{x})$ , which step 1.1 rewrites as $((\partial_{x} f) F_{y} - (\partial_{y} f) F_{x}) + f (\partial_{x} F_{y} - \partial_{y} F_{x})$ . By [F2] and [F3] the first bracket is the third coordinate $u_{x} v_{y} - u_{y} v_{x}$ of $\nabla f \times F$ , and the second summand is $f$ times the third coordinate of $curl F$ .

3.1step 2.1step 2.2step 2.3step 2.4step 2.5step 2.6∎

Steps 2.4, 2.5 and 2.6 give the three coordinates of $\nabla f \times F + f curl F$ , so $curl (f F) = \nabla f \times F + f curl F$ ; with steps 2.1, 2.2 and 2.3 this is every assertion of the Statement.

Remarks

The scalar $f$ need only be $C^{1}$ . No mixed second derivative of $f$ appears in either product rule, so nothing here needs $C^{2}$ ; the identities of The curl of the gradient of a $C^{2}$ function vanishes and The divergence of the curl of a $C^{2}$ field vanishes are where the second-order hypothesis becomes necessary.

Depends on

Used by

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus (University of British Columbia), Theorems 4.1.4 and 4.1.5 (standard reference, not scraped)
M. Corral, Vector Calculus, chapter 4 (LibreTexts) (standard reference, not scraped)