Closed smooth differential two-forms

This module supplies the constant-form convenience theorem for smooth two-forms. The generic closedness predicate and its chartwise API are defined in DifferentialForm.Closed.

theorem TauCeti.SmoothTwoForm.isClosed_const {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (B : V →L[ℝ] V →L[ℝ] ℝ) : SmoothForm.IsClosed (const B)

Constant forms on a model space are closed.