OAI/NumberTheory/SiegelZeros/Differentials/FinrankDerivationCardTranscendenceBasis.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_derivation_eq_card_transcendenceBasis line 16
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_derivation_eq_trdeg_toENat line 45
  3. theorem OAI.SiegelZeros.WeightedTorusJets.finiteType_dimension_trdeg line 61
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ringKrullDim_eq_finrank_derivation line 83
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.comap_aeval_eq_bot_of_independent_quotient line 104
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_height line 126
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_localized_mem_minimalPrimes line 134
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.mvPolynomial_height_eq_card_iff_isMaximal line 174
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateLocalizedPrime_isPrime line 200
  10. theorem OAI.SiegelZeros.WeightedTorusJets.trdeg_eq_of_integral_polynomial_base line 213
  11. theorem OAI.SiegelZeros.WeightedTorusJets.fractionField_trdeg_eq_nat line 227
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_prime_height_add_quotient_dim_of_finite line 239
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_normalization_quotient_dimension_finite line 260
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_normalization_count_add_height_finite line 271
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_normalization_count_le_finite line 281
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_normalization_height_eq_sub_finite line 289