OAI/NumberTheory/Jacobsthal/Siegel/CoordinateLocalizedPrime.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.coordinateLocalizedPrime line 28
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateLocalizedPrime_height line 35
  3. def OAI.Erdos970.WeightedTorusJets.Geometry.coordinateFractionLocalEquiv line 46
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateFraction_localEquiv_algebraMap line 67
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateLocalizedPrime_finite_quotient line 101
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinate_complement_card_eq_height line 110
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_coordinate_localization line 121
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.ring_length_eq_of_ringEquiv line 154
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.quotient_length_eq_of_ringEquiv line 162
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.radical_map_ringEquiv_eq_maximalIdeal line 176
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.map_span_range_of_commuting_images line 187
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_length_eq_of_commuting_images line 195
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.radical_span_eq_maximalIdeal_of_commuting_images line 203
  14. def OAI.Erdos970.WeightedTorusJets.Geometry.polynomialRenameLocalEquiv line 211
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomialRename_localEquiv_algebraMap line 218
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.maximal_local_bound_of_card_eq line 234
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_parameter_bound_of_isLocalization_atPrime line 268
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.arbitrary_prime_bound_of_maximal_local_bound line 291
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.arbitrary_local_bound_of_maximal_local_bound line 331
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficient_residue_injective line 369
  21. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.componentCoefficientFractionAlgebra line 379
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.componentCoefficientFractionAlgebra_tower line 386
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.component_functionField_finite line 398
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_isMaximal_of_finite line 419
  25. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation line 459
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_symm_C_X line 464
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_symm_X line 469
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_coefficient_map line 474
  29. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentationQuotientEquiv line 491
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_coefficient_comap_eq_bot line 513
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.finite_normalizationPresentation_quotient line 526