isRegular_X_pow

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.isRegular_X_pow

English

Any power X_s^k is a regular element (non-zero divisor) in the multivariate polynomial ring.

Русский

Любая степень X_s^k — регулярный элемент (не делитель нуля) в кольце многочленов.

LaTeX

$$$IsRegular(X_s^k)$$$

Lean4

@[simp]
theorem isRegular_X_pow (k : ℕ) : IsRegular (X n ^ k : MvPolynomial σ R) :=
  isRegular_X.pow k

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

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

Разделы

Аффилиация

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