OAI/NumberTheory/SiegelZeros/LocalAlgebra/CoordinateLocalizedPrime.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateLocalizedPrime line 23
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateLocalizedPrime_height line 30
  3. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateFractionLocalEquiv line 41
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateFraction_localEquiv_algebraMap line 62
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateLocalizedPrime_finite_quotient line 96
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinate_complement_card_eq_height line 105
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_coordinate_localization line 116
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.ring_length_eq_of_ringEquiv line 149
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.quotient_length_eq_of_ringEquiv line 157
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.radical_map_ringEquiv_eq_maximalIdeal line 171
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.map_span_range_of_commuting_images line 182
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_length_eq_of_commuting_images line 190
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.radical_span_eq_maximalIdeal_of_commuting_images line 198
  14. def OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialRenameLocalEquiv line 206
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialRename_localEquiv_algebraMap line 213
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.maximal_local_bound_of_card_eq line 229
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_parameter_bound_of_isLocalization_atPrime line 263
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.arbitrary_prime_bound_of_maximal_local_bound line 286
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.arbitrary_local_bound_of_maximal_local_bound line 326
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficient_residue_injective line 362
  21. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.componentCoefficientFractionAlgebra line 372
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.componentCoefficientFractionAlgebra_tower line 379
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.component_functionField_finite line 391
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_isMaximal_of_finite line 412
  25. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation line 451
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_symm_C_X line 456
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_symm_X line 461
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_coefficient_map line 466
  29. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentationQuotientEquiv line 483
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_coefficient_comap_eq_bot line 505
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.finite_normalizationPresentation_quotient line 518