OAI/NumberTheory/Jacobsthal/Siegel/TorusEvalOne.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_independent_normal_finset_algebraMap line 20
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.cotangent_finrank_add_logarithmic_tangent_finrank line 50
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_selected_independent_normal_coordinates line 74
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateNormal_invariant_functional_eq line 108
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_selected_independent_conormal_derivations line 124
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_logarithmicForm_ne_zero_of_cotangent_le_three line 166
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_selected_independent_conormal_derivations_atPrime line 198
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_selected_first_order_taylor_parameters_atPrime line 222
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.invariantDerivation_commute line 253
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localization_derivation_ext line 270
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.iterate_localizeDerivation_algebraMap line 286
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localizeDerivation_commute line 295
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.mixed_localizeDerivation_algebraMap line 310
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_algebraMap_injective line 326
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_polynomial_ne_zero line 333
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_coordinate_isUnit line 338
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.component_local_radical line 360
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.component_local_primary line 366
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.component_local_contains_maximal_pow line 372
  20. def OAI.Erdos970.WeightedTorusJets.Geometry.torusEvalOne line 384
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusEvalOne_algebraMap line 390
  22. def OAI.Erdos970.WeightedTorusJets.Geometry.torusIdentityPoint line 397
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJetIdeal_mono line 404
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJetIdeal_zero line 410
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJetZeroLocus_antitone line 424
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJetIdeal_le_ker line 429
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_consecutive_eq_of_dimension_bound line 437
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isIrreducible_subtype_preimage line 456
  29. def OAI.Erdos970.WeightedTorusJets.Geometry.irreducibleClosedSubtypeEmbedding line 471
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_irreducible_dimension_nat line 481
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localization_ringKrullDim_le line 503
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.hypersurface_ringKrullDim_le line 509
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.four_variable_localization_ringKrullDim_le line 516
  34. theorem OAI.Erdos970.WeightedTorusJets.Geometry.vanishingIdeal_isMinimalPrime_of_maximal line 523
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_shared_maximal_of_krullDim_eq_with_height line 538
  36. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_irreducible_dimension_eq_order_height line 565
  37. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_shared_component_of_full_local_dimension line 580
  38. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_shared_component_of_dimension_three_full line 613
  39. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJets_have_shared_component_full line 660
  40. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJets_have_shared_minimal_prime line 697