Theorem IsReduced.pow_ne_zero

Modification history

2024-09-29 21:20
Mathlib/RingTheory/Nilpotent/Defs.lean
feat(AlgebraicGeometry/EllipticCurve/Weierstrass): add `j_eq_zero[_iff][']` (#16974) …
Added IsReduced.pow_ne_zeroView on Github →