OAI/MathematicalPhysics/PEPSMove/SpectralPowers.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialPEPS.PhysicalMove.SpectralCurve.spectralHom line 17
2. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralCurve.spectralHom_apply line 27
3. def OAI.PolynomialPEPS.PhysicalMove.SupportedCurve.scalar line 37
4. def OAI.PolynomialPEPS.PhysicalMove.SupportedCurve.power line 40
5. theorem OAI.PolynomialPEPS.PhysicalMove.SupportedCurve.scalar_real line 43
6. theorem OAI.PolynomialPEPS.PhysicalMove.SupportedCurve.norm_scalar_imaginary line 54
7. theorem OAI.PolynomialPEPS.PhysicalMove.SupportedCurve.norm_power_imaginary line 60
8. theorem OAI.PolynomialPEPS.PhysicalMove.SupportedCurve.hasDerivAt_scalar line 65
9. theorem OAI.PolynomialPEPS.PhysicalMove.SupportedCurve.hasDerivAt_power line 76
10. theorem OAI.PolynomialPEPS.PhysicalMove.SupportedCurve.power_real_eq_cfc line 87