OAI/NumberTheory/SiegelZeros/Differentials/InvariantDerivationLemmas.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.maximal_mvPolynomial_height line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.regular_local_maximal_height line 41
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_mem_submodule_notMem_ideals line 56
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_finset_mem_submodule_height line 72
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_parameters_in_submodule line 114
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_polynomial_parameters line 145
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_parameters_at_generic_point line 193
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_parameters_at_localized_generic_point line 222
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_length_antitone line 246
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_quotient_artinian_of_radical line 252
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_quotient_length_ne_top_of_radical line 259
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_parameters_with_finite_length line 270
  13. def OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantDerivation line 305
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantDerivation_monomial line 309
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coeff_invariantDerivation line 316
  16. def OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantJet line 330
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coeff_iterate_invariantDerivation line 336
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coeff_invariantJet line 346
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.support_invariantJet_subset line 354
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.totalDegree_invariantJet_le line 360