OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousComplexIndependence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Real independent physical vectors stay independent in the doubled space

  1. theorem OAI.DefocusingNLS.homogeneousComplexReal_smul_embed line 17
  2. theorem OAI.DefocusingNLS.homogeneousComplexImag_smul_embed line 26
  3. theorem OAI.DefocusingNLS.homogeneousComplexEmbed_linearIndependent line 35