OAI/AlgebraicGeometry/AbhyankarSathaye/Identities.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Polynomial identities for the cusp and the explicit hypersurface

The polynomials S and P give the identity (x + s³)² + (y - s²)³ = s * (1 + F). The Bézout certificate is valid over every commutative ring. In the ambient complex polynomial ring, the variables are ordered as h, u, v, w.

  1. def OAI.AbhyankarSathaye.S line 19

    Also declared: ComparatorChallenges/CommutingDerivations.lean:14 (same declaration text).

  2. def OAI.AbhyankarSathaye.P line 22

    Also declared: ComparatorChallenges/CommutingDerivations.lean:17 (same declaration text).

  3. def OAI.AbhyankarSathaye.Alpha line 25
  4. def OAI.AbhyankarSathaye.Beta line 28
  5. theorem OAI.AbhyankarSathaye.cusp_universal line 31
  6. theorem OAI.AbhyankarSathaye.shift_universal line 36
  7. theorem OAI.AbhyankarSathaye.bezout_certificate line 41
  8. abbrev OAI.AbhyankarSathaye.R line 47

    Also declared: ComparatorChallenges/CommutingDerivations.lean:20 (same declaration text).

  9. def OAI.AbhyankarSathaye.h line 49

    Also declared: ComparatorChallenges/CommutingDerivations.lean:22 (same declaration text).

  10. def OAI.AbhyankarSathaye.u line 50

    Also declared: ComparatorChallenges/CommutingDerivations.lean:23 (same declaration text).

  11. def OAI.AbhyankarSathaye.v line 51

    Also declared: ComparatorChallenges/CommutingDerivations.lean:24 (same declaration text).

  12. def OAI.AbhyankarSathaye.w line 52

    Also declared: ComparatorChallenges/CommutingDerivations.lean:25 (same declaration text).

  13. def OAI.AbhyankarSathaye.x line 53

    Also declared: ComparatorChallenges/CommutingDerivations.lean:26 (same declaration text).

  14. def OAI.AbhyankarSathaye.y line 54

    Also declared: ComparatorChallenges/CommutingDerivations.lean:27 (same declaration text).

  15. def OAI.AbhyankarSathaye.s line 55

    Also declared: ComparatorChallenges/CommutingDerivations.lean:28 (same declaration text).

  16. def OAI.AbhyankarSathaye.p line 56

    Also declared: ComparatorChallenges/CommutingDerivations.lean:29 (same declaration text).

  17. def OAI.AbhyankarSathaye.F line 57

    Also declared: ComparatorChallenges/CommutingDerivations.lean:30 (same declaration text).

  18. def OAI.AbhyankarSathaye.shiftX line 58
  19. def OAI.AbhyankarSathaye.shiftY line 59
  20. theorem OAI.AbhyankarSathaye.cusp line 61
  21. theorem OAI.AbhyankarSathaye.shift line 63
  22. theorem OAI.AbhyankarSathaye.ambient line 66