OAI/NumberTheory/SiegelZeros/Differentials/TorusDerivationOverRat.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_augmentation line 16
  2. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusDerivationOverRat line 37
  3. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localTorusDerivationOverRat line 42
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusDerivationOverRat_commute line 47
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localTorusDerivationOverRat_commute line 54
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_derivationJet_eq line 61
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_derivativeStageIdeal_eq line 68
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_torus_derivativeStageIdeal_eq line 74
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_torus_stage_le_maximal line 86
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_torus_stage_primary_data line 98
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationCotangentResidue_restrictScalars line 124
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localTorusDerivationOverRat_eq_direct line 141
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localTorusDerivationOverRat_cotangent_eq_direct line 156
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationJet_selected_one line 173
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationJet_selected_two line 188
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationJet_selected_three line 212