monomial_mem_nonzeroDivisors — Mathlib

English

A monomial m = monomial n r is a nonzero divisor in the mv power series ring iff r is a nonzero divisor in R.

Русский

Моном m = monomial n r является несократимым делителем в кольце mv power series тогда и только тогда, когда r является несократимым делителем в R.

LaTeX

$$$$\text{monomial}_{n}(r) \in (\mathrm{MvPowerSeries}(\sigma,R))^{0} \iff r \in R^{0}.$$$$

Lean4

theorem monomial_mem_nonzeroDivisors {n : σ →₀ ℕ} {r} : monomial n r ∈ (MvPowerSeries σ R)⁰ ↔ r ∈ R⁰ :=
  monomial_mem_nonzeroDivisorsLeft.and monomial_mem_nonzeroDivisorsRight

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