X_mem_nonzeroDivisors

Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.X_mem_nonzeroDivisors

English

The Basic indeterminate X_i belongs to the set of non-zero-divisors in the mv-power-series ring.

Русский

Индетерминант X_i принадлежит множеству не нулевых делителей в mv-ряде.

LaTeX

$$$X_i \in (\mathrm{MvPowerSeries}(\sigma,R))^{0}.$$$

Lean4

theorem X_mem_nonzeroDivisors {i : σ} : X i ∈ (MvPowerSeries σ R)⁰ :=
  by
  rw [X, monomial_mem_nonzeroDivisors]
  exact Submonoid.one_mem R⁰

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru