English
A monomial monomial n → f is a left non-zero-divisor in the mv-power-series ring if and only if its coefficient r is a left non-zero-divisor in R.
Русский
Мономиал с векторным индексом n и коэффициент r слева является нулевым делителем, тогда и только если r — левый нулевой делитель в R.
LaTeX
$$$\forall n:\, (\sigma\to\mathbb{N})\to0,\ \forall r,\monomial(n)\,r \in \mathrm{nonZeroDivisorsLeft}(\mathrm{MvPowerSeries}(\sigma,R)) \iff r\in \mathrm{nonZeroDivisorsLeft}(R).$$$
Lean4
theorem monomial_mem_nonzeroDivisorsLeft {n : σ →₀ ℕ} {r} :
monomial n r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisorsLeft R :=
by
constructor
· intro H s hrs
have := H (C s) (by rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs])
simpa using congr(coeff 0 $(this))
· intro H p hrp
ext i
have := congr(coeff (i + n) $hrp)
rw [coeff_monomial_mul, if_pos le_add_self, add_tsub_cancel_right] at this
simpa using H _ this
