OAI/NumberTheory/Jacobsthal/Siegel/InvariantDerivation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.maximal_mvPolynomial_height line 20
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.regular_local_maximal_height line 42
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_mem_submodule_notMem_ideals line 57
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_finset_mem_submodule_height line 73
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_parameters_in_submodule line 115
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_polynomial_parameters line 146
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_parameters_at_generic_point line 194
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_parameters_at_localized_generic_point line 223
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_length_antitone line 247
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_quotient_artinian_of_radical line 253
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_quotient_length_ne_top_of_radical line 260
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_parameters_with_finite_length line 271
  13. def OAI.Erdos970.WeightedTorusJets.Geometry.invariantDerivation line 306
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.invariantDerivation_monomial line 310
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coeff_invariantDerivation line 317
  16. def OAI.Erdos970.WeightedTorusJets.Geometry.invariantJet line 331
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coeff_iterate_invariantDerivation line 337
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coeff_invariantJet line 347
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.support_invariantJet_subset line 355
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.totalDegree_invariantJet_le line 361