OAI/NumberTheory/Jacobsthal/Siegel/PolynomialLaurent.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.polynomialToLaurent line 22
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomialToLaurent_X line 25
  3. def OAI.Erdos970.WeightedTorusJets.Geometry.localizationToLaurent line 32
  4. def OAI.Erdos970.WeightedTorusJets.Geometry.localizedCoordinateUnit line 39
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localizedCoordinateUnit_val line 43
  6. def OAI.Erdos970.WeightedTorusJets.Geometry.localizedExponentHom line 47
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localizedExponentHom_single line 52
  8. def OAI.Erdos970.WeightedTorusJets.Geometry.laurentToLocalization line 57
  9. def OAI.Erdos970.WeightedTorusJets.Geometry.laurentEquivLocalization line 61
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurentEquivLocalization_coordinate line 71
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.prime_height_eq_under_of_integral_goingDown line 84
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.maximal_height_eq_ringKrullDim_of_finiteType line 110
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.altitude_of_relative_fraction_fields line 136
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_injective_polynomial_quotient_lift line 164
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_quotient_lift_properties line 181
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localized_prime_isMaximal_of_quotient_integral line 216
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.relative_denominators_le_nonZeroDivisors line 251
  18. abbrev OAI.Erdos970.WeightedTorusJets.Geometry.relativeLocalizationFractionAlgebra line 256
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.relativeLocalizationFraction_scalarTower line 265
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.relativeLocalization_fractionBase_scalarTower line 277
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.prime_height_add_quotient_dim_eq_of_finiteType line 292
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localization_mvPolynomial_ringKrullDim_le line 342
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_chart_ringKrullDim line 353
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_component_cotangent_eq_codimension line 382
  25. def OAI.Erdos970.WeightedTorusJets.Geometry.localizationResidueAlgEquiv line 424
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localization_residue_algEquiv_algebraMap line 431
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localization_residue_isFractionRing line 438
  28. def OAI.Erdos970.WeightedTorusJets.Geometry.localizationResidueQuotientAlgebra line 449
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localization_residue_quotientAlgebra_data line 456
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localization_residue_quotientAlgebra_mk line 470