OAI/NumberTheory/SiegelZeros/EntireFunctions/TorusJetZeroSchemeInclusion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusJetZeroSchemeInclusion line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusJetZeroSchemeInclusion_isClosedImmersion line 25
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusJetZeroScheme_component_genericPoint line 30
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_maximal_ideal_isNilpotent line 53
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.spec_stalk_component_filtration_nilpotent line 67
  6. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localizationQuotientEquivStalkQuotient line 82
  7. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeStalkEquivAmbientQuotient line 91
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeStalk_length_ambientStalk line 99
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ambient_stalk_quotient_length_eq_localization line 112
  10. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusToPolynomialFractionRing line 130
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusToPolynomialFractionRing_algebraMap line 139
  12. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusPolynomialFractionAlgebra line 146
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusPolynomialFractionAlgebra_data line 151
  14. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusFractionRingEquiv line 168
  15. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusFractionRingEquivOverK line 182
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusFractionRingEquivOverK_algebraMap line 195