OAI/NumberTheory/SiegelZeros/Differentials/SelectedCotangent.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.W18.derivationDualHom line 27
  2. def OAI.SiegelZeros.WeightedTorusJets.W18.localizedDualHom line 48
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localizedDualHom_algebraMap line 52
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localizedDualHom_fst line 57
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localizedDualHom_scalar_snd line 69
  6. def OAI.SiegelZeros.WeightedTorusJets.W18.localizedDerivation line 74
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localizedDerivation_algebraMap line 84
  8. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localizedDerivation_mk'_denominator line 91
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localizedDerivation_mk' line 102
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localization_derivation_ext line 125
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localizedDerivation_commute line 138
  12. theorem OAI.SiegelZeros.W58.ideal_smul_quotient_zero line 160
  13. def OAI.SiegelZeros.W58.normalRestriction line 165
  14. theorem OAI.SiegelZeros.W58.normalRestriction_product_zero line 172
  15. def OAI.SiegelZeros.W58.conormalPairing line 176
  16. theorem OAI.SiegelZeros.W58.conormalPairing_toCotangent line 179
  17. instance OAI.SiegelZeros.W58.cotangentQuotientScalarTower line 182
  18. def OAI.SiegelZeros.W58.residueConormalPairing line 185
  19. theorem OAI.SiegelZeros.W58.residueConormalPairing_apply line 189
  20. theorem OAI.SiegelZeros.W58.residueConormalPairing_toCotangent line 192
  21. theorem OAI.SiegelZeros.W58.residueConormalPairing_restrictScalars line 195
  22. def OAI.SiegelZeros.W58.reducedDerivation line 200
  23. theorem OAI.SiegelZeros.W58.reducedDerivation_apply line 203
  24. def OAI.SiegelZeros.W58.derivationNormal line 206
  25. theorem OAI.SiegelZeros.W58.derivationNormal_toCotangent line 209
  26. def OAI.SiegelZeros.WeightedTorusJets.W18.torusDerivation line 220
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W18.torusDerivation_polynomial line 224
  28. theorem OAI.SiegelZeros.WeightedTorusJets.W18.torusDerivation_commute line 229
  29. instance OAI.SiegelZeros.WeightedTorusJets.W18.(instance at line 233) line 233
  30. def OAI.SiegelZeros.WeightedTorusJets.W18.localTorusDerivation line 238
  31. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localTorusDerivation_algebraMap line 243
  32. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localTorusDerivation_commute line 250
  33. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localTorusDerivation_polynomial line 257
  34. theorem OAI.SiegelZeros.WeightedTorusJets.W18.localTorusDerivation_quotient line 266
  35. abbrev OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.LocalRing line 284
  36. abbrev OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.Residue line 289
  37. abbrev OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.Maximal line 290
  38. abbrev OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.Cotangent line 291
  39. def OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.identityResidueEquiv line 300
  40. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.identityResidueEquiv_base line 304
  41. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.identityResidueEquiv_scalar line 313
  42. def OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.identityResidueAlgEquiv line 326
  43. def OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.localCoordinateDifference line 329
  44. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.localCoordinateDifference_mem line 332
  45. def OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.coordinateClass line 345
  46. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.identityIdeal_span line 349
  47. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.maximal_span line 385
  48. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.coordinateClass_span line 410
  49. def OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.invariantNormal line 421
  50. lemma OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.invariantDerivation_X line 425
  51. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.local_derivative_coordinate line 437
  52. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.residue_coordinate line 461
  53. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.invariantNormal_coordinateClass line 473
  54. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.coordinate_normal_pairing line 481
  55. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.coordinateClass_linearIndependent line 488
  56. def OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.coordinateCotangentBasis line 496
  57. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.coordinateCotangentBasis_apply line 500
  58. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.identity_cotangent_finrank line 504
  59. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.invariantNormal_linearIndependent line 507
  60. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityCotangentRank.invariant_three_normal_rank line 528
  61. def OAI.SiegelZeros.Result.Workers.W57.rectangleFirst line 542
  62. theorem OAI.SiegelZeros.Result.Workers.W57.projection_surjective line 551
  63. theorem OAI.SiegelZeros.Result.Workers.W57.rectangleFirst_mul line 561
  64. def OAI.SiegelZeros.Result.Workers.W57.augmentationFirst line 580
  65. theorem OAI.SiegelZeros.Result.Workers.W57.augmentationFirst_product_zero line 587
  66. def OAI.SiegelZeros.Result.Workers.W57.augmentationCotangentCoefficient line 600
  67. theorem OAI.SiegelZeros.Result.Workers.W57.rectangleFirst_taylor line 609
  68. def OAI.SiegelZeros.Result.Workers.W57.rectangularJetAlgHom line 615
  69. theorem OAI.SiegelZeros.Result.Workers.W57.quotientTaylor_augmentation_comap line 620
  70. def OAI.SiegelZeros.Result.Workers.W57.sourceTaylorCotangent line 630
  71. theorem OAI.SiegelZeros.Result.Workers.W57.sourceTaylorCotangent_coefficient line 644
  72. def OAI.SiegelZeros.Result.Workers.W57.selectedFirst line 660
  73. theorem OAI.SiegelZeros.Result.Workers.W57.selectedFirst_mul line 666
  74. def OAI.SiegelZeros.Result.Workers.W57.selectedAugmentationFirst line 691
  75. theorem OAI.SiegelZeros.Result.Workers.W57.selectedAugmentationFirst_product_zero line 698
  76. def OAI.SiegelZeros.Result.Workers.W57.selectedCotangentCoefficient line 710
  77. theorem OAI.SiegelZeros.Result.Workers.W57.selectedFirst_taylor line 718
  78. def OAI.SiegelZeros.Result.Workers.W57.selectedSourceTaylorCotangent line 724
  79. theorem OAI.SiegelZeros.Result.Workers.W57.selectedSourceTaylorCotangent_coefficient line 736