Commit 2024-09-29 21:20 301f54ab

View on Github →

feat(AlgebraicGeometry/EllipticCurve/Weierstrass): add j_eq_zero[_iff]['] (#16974) which state the equivalency of j = 0 and c4 ^ 3 = 0 (and c4 = 0 if the ring is reduced). Also added IsReduced.pow_(eq|ne)_zero[_iff], which generalizes the pow_(eq|ne)_zero[_iff] assuming NoZeroDivisors.

Estimated changes