Registry · Proposition IV.P08 tau-effective formalized

IV.P08 — Integrability Criterion

A CR-structure (H, J) is integrable if and only if the Nijenhuis tensor N_J vanishes on H. Equivalent to Lie bracket closure of Gamma(H^{1,0}).

Book IV Part 3 Ch. 16

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.CRAddressSpace

Symbol: Tau.BookIV.QuantumMechanics.IntegrabilityCriterion