OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPhysicalRealSpan.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Real and imaginary coordinates of the complex physical symmetry span

  1. theorem OAI.DefocusingNLS.homogeneousComplexReal_smul line 16
  2. theorem OAI.DefocusingNLS.homogeneousComplexImag_smul line 24
  3. theorem OAI.DefocusingNLS.homogeneousComplexEmbed_coordinates line 32
  4. theorem OAI.DefocusingNLS.homogeneous_frame_real_coordinates line 38