instNoZeroDivisors

Mathlib.Algebra.Polynomial.Basic

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

English

If R has no zero divisors, then the polynomial ring R[X] also has no zero divisors.

Русский

Если R не имеет нулевых делителей, то и R[X] не имеет нулевых делителей.

LaTeX

$$If NoZeroDivisors(R) then NoZeroDivisors(R[X]).$$

Lean4

instance [NoZeroDivisors R] : NoZeroDivisors R[X] :=
  (toFinsuppIso R).injective.noZeroDivisors _ (map_zero _) (map_mul _)

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

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

Разделы

Аффилиация

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