The exterior derivative of a constant differential form

A differential form on a normed space which does not depend on the base point has exterior derivative zero, within any set and at any point. This complements the linearity lemmas of Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean, which cover the 0-form case only (extDerivWithin_constOfIsEmpty), and is what makes constant two-forms on a vector space closed.

Main declarations

• ContinuousAlternatingMap.extDerivWithin_const and ContinuousAlternatingMap.extDeriv_const: the exterior derivative of a constant form vanishes.

@[simp]

theorem ContinuousAlternatingMap.extDerivWithin_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (ω : E [⋀^Fin n]→L[𝕜] F) (s : Set E) (x : E) : extDerivWithin (fun (x : E) => ω) s x = 0

The exterior derivative within a set of a constant differential form vanishes.

@[simp]

theorem ContinuousAlternatingMap.extDeriv_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (ω : E [⋀^Fin n]→L[𝕜] F) (x : E) : extDeriv (fun (x : E) => ω) x = 0

The exterior derivative of a constant differential form vanishes.