OAI/NumberTheory/SiegelZeros/Intersection/TorusEvalOne.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_independent_normal_finset_algebraMap line 17
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.cotangent_finrank_add_logarithmic_tangent_finrank line 47
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_selected_independent_normal_coordinates line 71
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateNormal_invariant_functional_eq line 105
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_selected_independent_conormal_derivations line 121
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_logarithmicForm_ne_zero_of_cotangent_le_three line 162
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_selected_independent_conormal_derivations_atPrime line 194
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_selected_first_order_taylor_parameters_atPrime line 218
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantDerivation_commute line 247
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localization_derivation_ext line 264
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.iterate_localizeDerivation_algebraMap line 280
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localizeDerivation_commute line 289
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.mixed_localizeDerivation_algebraMap line 304
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_algebraMap_injective line 320
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_polynomial_ne_zero line 327
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_coordinate_isUnit line 332
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.component_local_radical line 349
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.component_local_primary line 355
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.component_local_contains_maximal_pow line 361
  20. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusEvalOne line 373
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusEvalOne_algebraMap line 379
  22. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusIdentityPoint line 386
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJetIdeal_mono line 393
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJetIdeal_zero line 399
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJetZeroLocus_antitone line 413
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJetIdeal_le_ker line 418
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_consecutive_eq_of_dimension_bound line 426
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isIrreducible_subtype_preimage line 445
  29. def OAI.SiegelZeros.WeightedTorusJets.Geometry.irreducibleClosedSubtypeEmbedding line 460
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_irreducible_dimension_nat line 470
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localization_ringKrullDim_le line 492
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.hypersurface_ringKrullDim_le line 498
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.four_variable_localization_ringKrullDim_le line 505
  34. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.vanishingIdeal_isMinimalPrime_of_maximal line 512
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_shared_maximal_of_krullDim_eq_with_height line 527
  36. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_irreducible_dimension_eq_order_height line 554
  37. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_shared_component_of_full_local_dimension line 569
  38. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_shared_component_of_dimension_three_full line 602
  39. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJets_have_shared_component_full line 649
  40. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJets_have_shared_minimal_prime line 686