Theorem IsReduced.pow_ne_zero

Modification history

2026-01-13 09:55
Mathlib/RingTheory/Nilpotent/Defs.lean
chore(Algebra): deduplicate `IsReduced` lemmas (#33775) …
Deleted IsReduced.pow_ne_zeroView on Github →
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 →