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
.