OAI/NumberTheory/Jacobsthal/Siegel/TorusDerivationOverRat.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_augmentation line 17
  2. def OAI.Erdos970.WeightedTorusJets.Geometry.torusDerivationOverRat line 38
  3. def OAI.Erdos970.WeightedTorusJets.Geometry.localTorusDerivationOverRat line 43
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusDerivationOverRat_commute line 48
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localTorusDerivationOverRat_commute line 55
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_derivationJet_eq line 62
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_derivativeStageIdeal_eq line 69
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_torus_derivativeStageIdeal_eq line 75
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_torus_stage_le_maximal line 87
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_torus_stage_primary_data line 99
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationCotangentResidue_restrictScalars line 125
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localTorusDerivationOverRat_eq_direct line 142
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localTorusDerivationOverRat_cotangent_eq_direct line 157
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationJet_selected_one line 174
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationJet_selected_two line 189
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationJet_selected_three line 213