OAI/NumberTheory/Jacobsthal/Siegel/FractionEulerDerivation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.biquadratic_torus_log_pairing line 14
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.lift_logarithmicForm_localize_invariantDerivation line 52
  3. theorem OAI.Erdos970.WeightedTorusJets.biquadratic_functionField_logarithmicForm_contraction line 71
  4. theorem OAI.Erdos970.WeightedTorusJets.biquadratic_functionField_contraction_zero_iff line 90
  5. theorem OAI.Erdos970.WeightedTorusJets.biquadratic_mem_span_iff_functionField_contraction_zero line 108
  6. def OAI.Erdos970.WeightedTorusJets.Geometry.fractionEulerDerivation line 128
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicTangentMap_fractionEulerDerivation line 133
  8. def OAI.Erdos970.WeightedTorusJets.Geometry.fractionInvariantDerivationLinearMap line 147
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicTangentMap_fractionInvariantDerivation line 154
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicTangentMap_injective_polynomial_fraction line 164
  11. def OAI.Erdos970.WeightedTorusJets.Geometry.fractionLogarithmicTangentEquiv line 183
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.fractionLogarithmicTangentEquiv_localize_invariantDerivation line 199
  13. def OAI.Erdos970.WeightedTorusJets.Geometry.fractionLogarithmicContractionLinearMap line 212
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.fractionLogarithmicContraction_eq_dotProduct_comp line 227
  15. theorem OAI.Erdos970.WeightedTorusJets.biquadratic_functionField_derivations_span_eq_ker line 241
  16. theorem OAI.Erdos970.WeightedTorusJets.biquadratic_functionField_derivations_linearIndependent line 273
  17. def OAI.Erdos970.WeightedTorusJets.biquadraticFunctionFieldDerivationBasis line 297
  18. theorem OAI.Erdos970.WeightedTorusJets.coe_biquadraticFunctionFieldDerivationBasis line 305