OAI/NumberTheory/SiegelZeros/Differentials/FractionEulerDerivation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.biquadratic_torus_log_pairing line 13
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.lift_logarithmicForm_localize_invariantDerivation line 51
  3. theorem OAI.SiegelZeros.WeightedTorusJets.biquadratic_functionField_logarithmicForm_contraction line 70
  4. theorem OAI.SiegelZeros.WeightedTorusJets.biquadratic_functionField_contraction_zero_iff line 91
  5. theorem OAI.SiegelZeros.WeightedTorusJets.biquadratic_mem_span_iff_functionField_contraction_zero line 109
  6. def OAI.SiegelZeros.WeightedTorusJets.Geometry.fractionEulerDerivation line 129
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicTangentMap_fractionEulerDerivation line 134
  8. def OAI.SiegelZeros.WeightedTorusJets.Geometry.fractionInvariantDerivationLinearMap line 148
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicTangentMap_fractionInvariantDerivation line 155
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicTangentMap_injective_polynomial_fraction line 165
  11. def OAI.SiegelZeros.WeightedTorusJets.Geometry.fractionLogarithmicTangentEquiv line 184
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.fractionLogarithmicTangentEquiv_localize_invariantDerivation line 200
  13. def OAI.SiegelZeros.WeightedTorusJets.Geometry.fractionLogarithmicContractionLinearMap line 213
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.fractionLogarithmicContraction_eq_dotProduct_comp line 228
  15. theorem OAI.SiegelZeros.WeightedTorusJets.biquadratic_functionField_derivations_span_eq_ker line 242
  16. theorem OAI.SiegelZeros.WeightedTorusJets.biquadratic_functionField_derivations_linearIndependent line 276
  17. def OAI.SiegelZeros.WeightedTorusJets.biquadraticFunctionFieldDerivationBasis line 300
  18. theorem OAI.SiegelZeros.WeightedTorusJets.coe_biquadraticFunctionFieldDerivationBasis line 308