X_mem_nonzeroDivisors

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

The indeterminate X is a zerodivisor-free element of the polynomial ring R[X].

Русский

Индетерминант X не является нулевым делителем в кольце полиномов R[X].

LaTeX

$$$ X \in R[X]^{0} $$$

Lean4

theorem X_mem_nonzeroDivisors : X ∈ R[X]⁰ :=
  mem_nonzeroDivisors_of_coeff_mem 1 (by simp [one_mem])

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

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

Разделы

Аффилиация

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