OAI/NumberTheory/Jacobsthal/Siegel/FinrankDerivationCardTranscendenceBasis.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_derivation_eq_card_transcendenceBasis line 19
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_derivation_eq_trdeg_toENat line 48
  3. theorem OAI.Erdos970.WeightedTorusJets.finiteType_dimension_trdeg line 64
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ringKrullDim_eq_finrank_derivation line 86
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.comap_aeval_eq_bot_of_independent_quotient line 107
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_height line 132
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_localized_mem_minimalPrimes line 140
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.mvPolynomial_height_eq_card_iff_isMaximal line 180
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateLocalizedPrime_isPrime line 209
  10. theorem OAI.Erdos970.WeightedTorusJets.trdeg_eq_of_integral_polynomial_base line 222
  11. theorem OAI.Erdos970.WeightedTorusJets.fractionField_trdeg_eq_nat line 236
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_prime_height_add_quotient_dim_of_finite line 248
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_normalization_quotient_dimension_finite line 269
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_normalization_count_add_height_finite line 280
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_normalization_count_le_finite line 290
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_normalization_height_eq_sub_finite line 298