OAI/MathematicalPhysics/Transonic/Certificates/Window43.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SepticProfile.ExteriorCertificates.C43.power_step line 11
2. theorem OAI.SepticProfile.ExteriorCertificates.C43.upper_eq line 86
3. theorem OAI.SepticProfile.ExteriorCertificates.C43.rprod_eq line 161
4. theorem OAI.SepticProfile.ExteriorCertificates.C43.rprod_pos line 235
5. theorem OAI.SepticProfile.ExteriorCertificates.C43.mono_step line 309
6. theorem OAI.SepticProfile.ExteriorCertificates.C43.signed_eq line 383
7. theorem OAI.SepticProfile.ExteriorCertificates.C43.signed_zero line 458
8. theorem OAI.SepticProfile.ExteriorCertificates.C43.signed_tail line 459
9. theorem OAI.SepticProfile.ExteriorCertificates.C43.poly_zero line 460
10. theorem OAI.SepticProfile.ExteriorCertificates.C43.poly_eq line 461
11. theorem OAI.SepticProfile.ExteriorCertificates.C43.square_eq line 466
12. theorem OAI.SepticProfile.ExteriorCertificates.C43.square_tail line 615
13. theorem OAI.SepticProfile.ExteriorCertificates.C43.cube_eq line 616
14. theorem OAI.SepticProfile.ExteriorCertificates.C43.cube_tail line 838
15. theorem OAI.SepticProfile.ExteriorCertificates.C43.fourth_eq line 839
16. theorem OAI.SepticProfile.ExteriorCertificates.C43.fourth_tail line 1134
17. theorem OAI.SepticProfile.ExteriorCertificates.C43.powers line 1135
18. theorem OAI.SepticProfile.ExteriorCertificates.C43.residual_eq line 1137
19. theorem OAI.SepticProfile.ExteriorCertificates.C43.panels line 1359
20. def OAI.SepticProfile.ExteriorCertificates.C43.window line 1393
21. theorem OAI.SepticProfile.ExteriorCertificates.C43.window_valid line 1394
22. theorem OAI.SepticProfile.ExteriorCertificates.C43.produces line 1426