isRegular_X

Mathlib.Algebra.Polynomial.Coeff

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

English

The polynomial X is a non-zero divisor in R[X]; i.e., if X · P = X · Q then P = Q.

Русский

Полином X является неабсолютным делителем в R[X]; то есть если X · P = X · Q, то P = Q.

LaTeX

$$$$\text{IsRegular}(X)$$$$

Lean4

@[simp]
theorem isRegular_X : IsRegular (X : R[X]) :=
  pow_one (X : R[X]) ▸ isRegular_X_pow 1

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

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

Разделы

Аффилиация

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