OAI/Analysis/Laughlin/Fock/EnergyRotation.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.Fock.sourceFockEnergy_eq_finline 10 - theorem
OAI.Laughlin.Fock.sourceFockEnergy_rotationline 16 - theorem
OAI.Laughlin.Fock.sourceFockHamiltonian_apply_finline 25 - theorem
OAI.Laughlin.Fock.sourceFockHamiltonian_rotationline 32