OAI/MathematicalPhysics/DefocusingNLS/Linear/SemigroupGeneratorEigenvector.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A real generator eigenvector evolves by its scalar exponential

  1. theorem OAI.DefocusingNLS.semigroup_eigenvector_of_generator line 14