OAI/Analysis/Laughlin/Charge/LaughlinGround.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.haldaneKernelInput line 8
  2. def OAI.Laughlin.Charge.physicalLaughlin line 16
  3. theorem OAI.Laughlin.Charge.physicalLaughlin_sector line 20
  4. theorem OAI.Laughlin.Charge.physicalLaughlin_ne_zero line 25
  5. theorem OAI.Laughlin.Charge.physicalLaughlin_zero_energy line 39
  6. theorem OAI.Laughlin.Charge.normalizedTensorExterior_smul line 46
  7. theorem OAI.Laughlin.Charge.physical_kernel_eq_laughlin line 50
  8. theorem OAI.Laughlin.Charge.physical_groundKernel_finrank line 73
  9. theorem OAI.Laughlin.Charge.physicalLaughlin_unit_zero_mode line 85
  10. theorem OAI.Laughlin.Charge.laughlinChargeGroundInput line 97