English
A monomial monomial n → f is a right non-zero-divisor in the mv-power-series ring if and only if its coefficient r is a right non-zero-divisor in R.
Русский
Мономиал с индексом n и коэффициентом r является правым нулевым делителем тогда и только если r — правый нулевой делитель в R.
LaTeX
$$$\forall n:\, (\sigma\to\mathbb{N})\to0,\ \forall r,\monomial(n)\,r \in \mathrm{nonZeroDivisorsRight}(\mathrm{MvPowerSeries}(\sigma,R)) \iff r\in \mathrm{nonZeroDivisorsRight}(R).$$$
Lean4
theorem monomial_mem_nonzeroDivisorsRight {n : σ →₀ ℕ} {r} :
monomial n r ∈ nonZeroDivisorsRight (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisorsRight 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_mul_monomial, if_pos le_add_self, add_tsub_cancel_right] at this
simpa using H _ this
