feat(AlgebraicGeometry/EllipticCurve/Weierstrass): add `j_eq_zero[_if…

…f][']` (#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`.

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

@@ -554,6 +554,16 @@ variable (E : EllipticCurve R)
 def j : R :=
   E.Δ'⁻¹ * E.c₄ ^ 3
 
+/-- A variant of `EllipticCurve.j_eq_zero_iff` without assuming the ring being reduced. -/
+lemma j_eq_zero_iff' : E.j = 0 ↔ E.c₄ ^ 3 = 0 := by
+  rw [j, Units.mul_right_eq_zero]
+
+lemma j_eq_zero (h : E.c₄ = 0) : E.j = 0 := by
+  rw [j_eq_zero_iff', h, zero_pow three_ne_zero]
+
+lemma j_eq_zero_iff [IsReduced R] : E.j = 0 ↔ E.c₄ = 0 := by
+  rw [j_eq_zero_iff', IsReduced.pow_eq_zero_iff three_ne_zero]
+
 lemma twoTorsionPolynomial_disc_ne_zero [Nontrivial R] [Invertible (2 : R)] :
     E.twoTorsionPolynomial.disc ≠ 0 :=
   E.toWeierstrassCurve.twoTorsionPolynomial_disc_ne_zero <| E.coe_Δ' ▸ E.Δ'.isUnit

Mathlib/RingTheory/Nilpotent/Defs.lean

@@ -168,6 +168,29 @@ class IsReduced (R : Type*) [Zero R] [Pow R ℕ] : Prop where
   /-- A reduced structure has no nonzero nilpotent elements. -/
   eq_zero : ∀ x : R, IsNilpotent x → x = 0
 
+namespace IsReduced
+
+theorem pow_eq_zero [Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) :
+    x = 0 := IsReduced.eq_zero x ⟨n, h⟩
+
+@[simp]
+theorem pow_eq_zero_iff [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) :
+    x ^ n = 0 ↔ x = 0 := ⟨pow_eq_zero, fun h ↦ h.symm ▸ zero_pow hn⟩
+
+theorem pow_ne_zero_iff [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) :
+    x ^ n ≠ 0 ↔ x ≠ 0 := not_congr (pow_eq_zero_iff hn)
+
+theorem pow_ne_zero [Zero R] [Pow R ℕ] [IsReduced R] (n : ℕ) (h : x ≠ 0) :
+    x ^ n ≠ 0 := fun H ↦ h (pow_eq_zero H)
+
+/-- A variant of `IsReduced.pow_eq_zero_iff` assuming `R` is not trivial. -/
+@[simp]
+theorem pow_eq_zero_iff' [MonoidWithZero R] [IsReduced R] [Nontrivial R] {n : ℕ} :
+    x ^ n = 0 ↔ x = 0 ∧ n ≠ 0 := by
+  cases n <;> simp
+
+end IsReduced
+
 instance (priority := 900) isReduced_of_noZeroDivisors [MonoidWithZero R] [NoZeroDivisors R] :
     IsReduced R :=
   ⟨fun _ ⟨_, hn⟩ => pow_eq_zero hn⟩