OAI/NumberTheory/Jacobsthal/Siegel/TorusJetZeroSchemeInclusion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.torusJetZeroSchemeInclusion line 20
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusJetZeroSchemeInclusion_isClosedImmersion line 26
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusJetZeroScheme_component_genericPoint line 31
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_maximal_ideal_isNilpotent line 48
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.spec_stalk_component_filtration_nilpotent line 60
  6. def OAI.Erdos970.WeightedTorusJets.Geometry.localizationQuotientEquivStalkQuotient line 75
  7. def OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeStalkEquivAmbientQuotient line 84
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeStalk_length_ambientStalk line 92
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ambient_stalk_quotient_length_eq_localization line 105
  10. def OAI.Erdos970.WeightedTorusJets.Geometry.torusToPolynomialFractionRing line 123
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusToPolynomialFractionRing_algebraMap line 132
  12. def OAI.Erdos970.WeightedTorusJets.Geometry.torusPolynomialFractionAlgebra line 139
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusPolynomialFractionAlgebra_data line 144
  14. def OAI.Erdos970.WeightedTorusJets.Geometry.torusFractionRingEquiv line 161
  15. def OAI.Erdos970.WeightedTorusJets.Geometry.torusFractionRingEquivOverK line 175
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusFractionRingEquivOverK_algebraMap line 188