OAI/NumberTheory/SiegelZeros/Intersection/IsolatedBezoutFromRegularSelection.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.W22.LocalIsolatedBezoutStatement line 25
  2. theorem OAI.SiegelZeros.W20.local_length_le_of_local_isolated_bezout line 49
  3. theorem OAI.SiegelZeros.W23.quotient_length_eq_of_ringEquiv line 104
  4. def OAI.SiegelZeros.W23.polynomialComponentPrime line 128
  5. instance OAI.SiegelZeros.W23.polynomialComponentPrime_isPrime line 131
  6. theorem OAI.SiegelZeros.W23.polynomialComponentPrime_mem_minimalPrimes line 134
  7. theorem OAI.SiegelZeros.W23.polynomialComponentPrime_height line 142
  8. def OAI.SiegelZeros.W23.polynomialTorusLocalEquiv line 146
  9. theorem OAI.SiegelZeros.W23.polynomialTorusLocalEquiv_algebraMap line 152
  10. theorem OAI.SiegelZeros.W23.torus_localized_ideal_eq_map_polynomial_localized line 159
  11. def OAI.SiegelZeros.W23.polynomialTorusLocalQuotientEquiv line 175
  12. theorem OAI.SiegelZeros.W23.polynomial_torus_local_quotient_length_eq line 186
  13. theorem OAI.SiegelZeros.W23.torus_local_length_le_of_local_isolated_bezout line 209
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W22.span_range_list_get line 247
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W22.span_range_map_list_get line 253
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W22.finiteLength_localized_minimal_quotient line 267
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W22.affine_local_regular_list_bezout line 287
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localIsolatedBezout_of_actual_regular_selection line 346