The difference of two variables is a non-zero-divisor

Mathlib shows that a single variable is a non-zero-divisor over an arbitrary semiring (MvPowerSeries.X_mem_nonZeroDivisors), and that MvPowerSeries σ R inherits NoZeroDivisors from R. Between those lies a gap: over a ring that has zero divisors, is X i - X j still regular? It is, and this file proves it.

Main results

• MvPowerSeries.X_sub_X_mem_nonZeroDivisors: for i ≠ j, the difference X i - X j is a non-zero-divisor of MvPowerSeries σ R over an arbitrary commutative ring.

Implementation notes

The proof is a coefficient recursion rather than a cancellation in R, which is what lets the hypotheses on R drop. Reading f * (X i - X j) = 0 at the exponent d + single i 1 gives coeff d f = coeff (d + single i 1 - single j 1) f when d j ≠ 0, and coeff d f = 0 when d j = 0, since the X j term is then absent for degree reasons. Each step lowers the j-exponent by one, so induction on d j walks every coefficient down to that base case.

theorem MvPowerSeries.X_sub_X_mem_nonZeroDivisors {σ : Type u_1} {R : Type u_2} [CommRing R] {i j : σ} (hij : i ≠ j) : X i - X j ∈ nonZeroDivisors (MvPowerSeries σ R)

The difference of two distinct variables is a non-zero-divisor, over an arbitrary commutative ring: f * (X i - X j) = 0 forces f = 0, with no hypothesis on R.

Compare MvPowerSeries.X_mem_nonZeroDivisors, the same statement for a single variable, and the NoZeroDivisors (MvPowerSeries σ R) instance, which requires R to have no zero divisors.