English
If the constant coefficient of φ lies in the left non-zero-divisors of R, then φ lies in the left non-zero-divisors of MvPowerSeries(σ,R).
Русский
Если константный коэффициент φ лежит в левом множестве неприводимых делителей нуля R, то φ лежит в левом множестве неприводимых делителей нуля MV-рядов.
LaTeX
$$$\bigl(\mathrm{constantCoeff}(\varphi)\in \mathrm{nonZeroDivisorsLeft}(R)\bigr) \Rightarrow (\varphi\in \mathrm{nonZeroDivisorsLeft}(\mathrm{MvPowerSeries}(\sigma,R))).$$$
Lean4
theorem mem_nonZeroDivisorsLeft_of_constantCoeff {φ : MvPowerSeries σ R}
(hφ : constantCoeff φ ∈ nonZeroDivisorsLeft R) : φ ∈ nonZeroDivisorsLeft (MvPowerSeries σ R) := by
classical
intro x hx
ext d
apply WellFoundedLT.induction d
intro e he
rw [map_zero, ← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ, ← map_zero (f := coeff e), ← hx]
convert (coeff_mul e φ x).symm
rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
· rintro ⟨_, u⟩ huv _
suffices u < e by simp only [he u this, mul_zero, map_zero]
apply lt_of_le_of_ne
· simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
· rintro rfl
simp_all
· simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff, false_implies]
