OAI/NumberTheory/SiegelZeros/LocalAlgebra/PolynomialLaurent.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialToLaurent line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialToLaurent_X line 22
  3. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localizationToLaurent line 29
  4. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localizedCoordinateUnit line 36
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localizedCoordinateUnit_val line 40
  6. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localizedExponentHom line 44
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localizedExponentHom_single line 49
  8. def OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentToLocalization line 54
  9. def OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentEquivLocalization line 58
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentEquivLocalization_coordinate line 68
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.prime_height_eq_under_of_integral_goingDown line 80
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.maximal_height_eq_ringKrullDim_of_finiteType line 106
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.altitude_of_relative_fraction_fields line 127
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_injective_polynomial_quotient_lift line 155
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_quotient_lift_properties line 172
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localized_prime_isMaximal_of_quotient_integral line 207
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.relative_denominators_le_nonZeroDivisors line 242
  18. abbrev OAI.SiegelZeros.WeightedTorusJets.Geometry.relativeLocalizationFractionAlgebra line 247
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.relativeLocalizationFraction_scalarTower line 256
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.relativeLocalization_fractionBase_scalarTower line 268
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.prime_height_add_quotient_dim_eq_of_finiteType line 283
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localization_mvPolynomial_ringKrullDim_le line 333
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_chart_ringKrullDim line 344
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_component_cotangent_eq_codimension line 373
  25. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localizationResidueAlgEquiv line 414
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localization_residue_algEquiv_algebraMap line 421
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localization_residue_isFractionRing line 428
  28. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localizationResidueQuotientAlgebra line 439
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localization_residue_quotientAlgebra_data line 446
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localization_residue_quotientAlgebra_mk line 460