OAI/MathematicalPhysics/DefocusingNLS/Certificates/FreePhysicalSymmetryNoChain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A simple determinant zero excludes chains of the physical H columns at every symmetry root, assuming the rectangle form of Rouché's theorem.

  1. theorem OAI.DefocusingNLS.radialFreePhysical_symmetry_no_chain line 16