OAI/NumberTheory/Jacobsthal/Siegel/FractionEquivAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ringKrullDim_away_eq_of_finiteType line 17
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.openImmersion_affine_topologicalKrullDim_eq line 41
  3. theorem OAI.Erdos970.WeightedTorusJets.exists_prime_fractionField_algEquiv_of_immersion line 78
  4. abbrev OAI.Erdos970.WeightedTorusJets.fractionEquivAlgebra line 150
  5. theorem OAI.Erdos970.WeightedTorusJets.fractionEquiv_isFractionRing_and_scalarTower line 153
  6. theorem OAI.Erdos970.WeightedTorusJets.quasiCompact_immersion_of_finiteType_affine line 167
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicForm_ne_zero_on_locallyClosed_torus_subvariety line 189
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicHyperplane_normal_rank_on_locallyClosed_torus_subvariety line 216
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusIdentity_tangent_coordinates line 285
  10. def OAI.Erdos970.WeightedTorusJets.Geometry.torusEvalPoint line 334
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusEvalPoint_algebraMap line 342
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_point_normal_equiv_rank line 348
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_torusEvalPoint_of_quotient_dimension_zero line 439