English
If the constant coefficient of φ is a right non-zero-divisor in R, then φ is a right non-zero-divisor in the mv-power-series ring.
Русский
Если константный коэффициент φ является правым неприводимым делителем нуля, то φ является правым неприводимым делителем нуля в кольце mv-рядов.
LaTeX
$$$\bigl(\mathrm{constantCoeff}(\varphi)\in \mathrm{nonZeroDivisorsRight}(R)\bigr) \Rightarrow (\varphi\in \mathrm{nonZeroDivisorsRight}(\mathrm{MvPowerSeries}(\sigma,R))).$$$
Lean4
theorem mem_nonZeroDivisorsRight_of_constantCoeff {φ : MvPowerSeries σ R}
(hφ : constantCoeff φ ∈ nonZeroDivisorsRight R) : φ ∈ nonZeroDivisorsRight (MvPowerSeries σ R) := by
classical
intro x hx
ext d
apply WellFoundedLT.induction d
intro e he
rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ, ← map_zero (f := coeff e), ← hx]
convert (coeff_mul e x φ).symm
rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
· rintro ⟨u, _⟩ huv _
suffices u < e by simp only [he u this, zero_mul, map_zero]
apply lt_of_le_of_ne
· simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
· rintro rfl
simp_all
·
simp only [mem_antidiagonal, add_zero, not_true_eq_false, coeff_zero_eq_constantCoeff, false_implies]
-- TODO: derive from `mem_nonZeroDivisorsRight_of_constantCoeff` using `MulOpposite`
