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.