OAI/NumberTheory/PowerFree/PairAlgebras.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.pairRelation line 9
  2. def OAI.QuarticPowerFree.PairNormal line 13
  3. theorem OAI.QuarticPowerFree.pair_normal_form line 16
  4. def OAI.QuarticPowerFree.pairExponent line 62
  5. theorem OAI.QuarticPowerFree.pairExponent_injective_normal line 65
  6. def OAI.QuarticPowerFree.pairLaurentMap line 107
  7. theorem OAI.QuarticPowerFree.pairLaurentMap_monomial line 114
  8. theorem OAI.QuarticPowerFree.pairLaurentMap_relation line 132
  9. theorem OAI.QuarticPowerFree.pairLaurentMap_normal_injective line 145
  10. theorem OAI.QuarticPowerFree.pair_ideal_eq_ker line 170
  11. theorem OAI.QuarticPowerFree.pair_ideal_isPrime line 197
  12. theorem OAI.QuarticPowerFree.pair_normal_quotient_bijective line 203
  13. def OAI.QuarticPowerFree.pairNormalEquiv line 234
  14. def OAI.QuarticPowerFree.pairNormalBasis line 243
  15. abbrev OAI.QuarticPowerFree.PairRing line 249
  16. def OAI.QuarticPowerFree.pairCoeffs line 252
  17. def OAI.QuarticPowerFree.pairScalePre line 256
  18. theorem OAI.QuarticPowerFree.pairScalePre_relation line 263
  19. def OAI.QuarticPowerFree.pairScale line 280
  20. theorem OAI.QuarticPowerFree.pairNormalBasis_apply line 292
  21. theorem OAI.QuarticPowerFree.aevalTower_monomial_homogeneous line 309
  22. theorem OAI.QuarticPowerFree.pairScale_monomial line 330
  23. theorem OAI.QuarticPowerFree.pairNormalBasis_smul line 353
  24. theorem OAI.QuarticPowerFree.pairBasis_homogeneous line 362
  25. def OAI.QuarticPowerFree.normPair_weightedLift line 377
  26. theorem OAI.QuarticPowerFree.normPair_weightedLift_monomial line 382
  27. def OAI.QuarticPowerFree.weightedScale line 397
  28. theorem OAI.QuarticPowerFree.weightedScale_monomial line 404
  29. theorem OAI.QuarticPowerFree.weightedScale_X line 410
  30. theorem OAI.QuarticPowerFree.weightedScale_C line 414
  31. def OAI.QuarticPowerFree.triplePairWeights line 418
  32. def OAI.QuarticPowerFree.pairConeQ line 420
  33. theorem OAI.QuarticPowerFree.pairConeQ_ne_zero line 424
  34. theorem OAI.QuarticPowerFree.pairConeQ_homogeneous line 435