OAI/NumberTheory/PowerFree/PairBoundaries.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuarticPowerFree.pairCone_mapped_equation line 10
  2. theorem OAI.QuarticPowerFree.quartic_pair_small_field line 29
  3. theorem OAI.QuarticPowerFree.pairAffine_bounded_cut_data line 68
  4. lemma OAI.QuarticPowerFree.pairCone_affine_eq_map line 116
  5. theorem OAI.QuarticPowerFree.quartic_bounded_pair_alternative line 135
  6. def OAI.QuarticPowerFree.pairBoundaryExponent line 194
  7. theorem OAI.QuarticPowerFree.pairBoundaryExponent_injective line 198
  8. def OAI.QuarticPowerFree.pairBoundaryMap line 212
  9. theorem OAI.QuarticPowerFree.pairBoundaryMap_monomial line 222
  10. theorem OAI.QuarticPowerFree.pairBoundaryMap_relation line 270
  11. theorem OAI.QuarticPowerFree.pairBoundaryMap_normal_coeff line 291
  12. theorem OAI.QuarticPowerFree.pair_boundary_ideal_eq_ker line 317
  13. theorem OAI.QuarticPowerFree.pair_boundary_ideal_isPrime line 380