mem_nonZeroDivisors_of_constantCoeff

English

A multivariate power series is a (two-sided) non-zero-divisor if its constant coefficient is a non-zero-divisor in R.

Русский

Мультимножество степенных рядов не является нулевым делителем в обоих направлениях, если константный коэффициент не является нулевым делителем в R.

LaTeX

$$$\varphi\in (\mathrm{MvPowerSeries}(\sigma,R))^{0} \quad\text{iff}\quad \mathrm{constantCoeff}(\varphi)\in R^{0}.$$$

Lean4

/-- A multivariate power series is not a zero divisor
  when its constant coefficient is not a zero divisor -/
theorem mem_nonZeroDivisors_of_constantCoeff {φ : MvPowerSeries σ R} (hφ : constantCoeff φ ∈ R⁰) :
    φ ∈ (MvPowerSeries σ R)⁰ :=
  ⟨mem_nonZeroDivisorsLeft_of_constantCoeff hφ.1, mem_nonZeroDivisorsRight_of_constantCoeff hφ.2⟩

Похожие утверждения