OAI/NumberTheory/SiegelZeros/LocalAlgebra/FractionEquivAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ringKrullDim_away_eq_of_finiteType line 16
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.openImmersion_affine_topologicalKrullDim_eq line 42
  3. theorem OAI.SiegelZeros.WeightedTorusJets.exists_prime_fractionField_algEquiv_of_immersion line 79
  4. abbrev OAI.SiegelZeros.WeightedTorusJets.fractionEquivAlgebra line 151
  5. theorem OAI.SiegelZeros.WeightedTorusJets.fractionEquiv_isFractionRing_and_scalarTower line 154
  6. theorem OAI.SiegelZeros.WeightedTorusJets.quasiCompact_immersion_of_finiteType_affine line 168
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicForm_ne_zero_on_locallyClosed_torus_subvariety line 190
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicHyperplane_normal_rank_on_locallyClosed_torus_subvariety line 217
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusIdentity_tangent_coordinates line 286
  10. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusEvalPoint line 335
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusEvalPoint_algebraMap line 343
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_point_normal_equiv_rank line 349
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_torusEvalPoint_of_quotient_dimension_zero line 440