OAI/Analysis/HardSphere/Rescaling/PhysicalUnitary.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HardSphere.Rescaling.pull_complex_smulline 13 - lemma
OAI.HardSphere.Rescaling.circle_inverseline 24 - lemma
OAI.HardSphere.Rescaling.config_inverseline 31 - lemma
OAI.HardSphere.Rescaling.jacobian_inverseline 36 - lemma
OAI.HardSphere.Rescaling.amplitude_inverseline 44 - lemma
OAI.HardSphere.Rescaling.pull_inverseline 51 - def
OAI.HardSphere.Rescaling.unitaryline 60 - lemma
OAI.HardSphere.Rescaling.unitary_applyline 69