fix(Tactic/Algebra): properly handle scalars that evaluate to zero (#39444)

When `algebra` encounters `0 • x` it gets normalized to `0 • x` instead of `0`, breaking the invariant that coefficients are not allowed to be zero. This PR fixes this issue and adds a corresponding test.

Author: amellendijk

Mathlib/Tactic/Algebra/Basic.lean

@@ -195,9 +195,14 @@ def cast (cR : Algebra.Cache sR) (u' : Level) (R' : Q(Type u'))
   let ⟨r, pf_smul⟩ ← evalSMulCast q($sAlg) q($_smul) r'
   let ⟨_r'', vr, pr⟩ ←
     Common.eval rcℕ (Ring.ringCompute cR.toCache) cR.toCache q($r)
-  assumeInstancesCommute
-  return ⟨_, Common.ExSum.add (Common.ExProd.const (.mk _ vr)) .zero,
-    q(cast_smul_eq_mul $pr $pf_smul)⟩
+  match vr with
+  | .zero .. =>
+    assumeInstancesCommute
+    return ⟨_, .zero, q(cast_zero_smul_eq_zero_mul $pr $pf_smul)⟩
+  | vr =>
+    assumeInstancesCommute
+    return ⟨_, Common.ExSum.add (Common.ExProd.const (.mk _ vr)) .zero,
+      q(cast_smul_eq_mul $pr $pf_smul)⟩
 
 /-- Evaluate the product of two normalized expressions in `R` using `ring`. -/
 def neg (cR : Algebra.Cache sR) {a : Q($A)} (_rA : Q(CommRing $A)) (za : BaseType sAlg a) :

Mathlib/Tactic/Algebra/Lemmas.lean

@@ -190,6 +190,12 @@ theorem add_algebraMap_isNat_zero {r s : R} (h : r + s = 0) :
   rw [← map_add, h, map_zero]
   exact ⟨by simp⟩
 
+/- RingCompute.cast -/
+theorem cast_zero_smul_eq_zero_mul {R' : Type*} [HSMul R' A A] {r' : R'} {r : R}
+    (hr : r = 0) (h_smul : ∀ (a : A), r • a = r' • a) (a : A) :
+    r' • a = (0 : A) * a := by
+  simp [← h_smul, hr]
+
 /- RingCompute.cast -/
 theorem cast_smul_eq_mul {R' : Type*} [HSMul R' A A] {r' : R'} {r r'' : R}
     (hr : r = r'') (h_smul : ∀ (a : A), r • a = r' • a) (a : A) :

MathlibTest/Algebra.lean

@@ -148,3 +148,7 @@ example {A R R' : Type*} [CommRing A] [CommRing R] [CommRing R'] [Algebra R A] [
 example {A R R' : Type*} [CommRing A] [CommRing R] [CommRing R'] [Algebra R A] [Algebra R' A] (r : R) (r' : R') (x : A) :
 (r : R) • x + (1 : ℕ) • x + (r' : R') • x = (r' : R') • x + (1 : ℕ) • x + (r : R) • x:= by
   algebra
+
+/- Ensure that terms are eliminated if the coefficient happens to evaluate to zero. -/
+example (x : ℚ) : 0 • x = 0 := by
+  algebra