isRegular_X_pow — Mathlib

English

For any natural n, X^n is a regular element (a non-zero divisor) in R[X] when R is a semiring; i.e., if X^n P = X^n Q then P = Q.

Русский

Для любого натурального n элемент X^n является неабсолюто-ненулевым делителем в R[X] при условии, что R — полугруппный полином; то есть X^n P = X^n Q ⇒ P = Q.

LaTeX

$$$$\forall P,Q\; (X^n P = X^n Q) \Rightarrow (P = Q)$$$$

Lean4

theorem isRegular_X_pow (n : ℕ) : IsRegular (X ^ n : R[X]) :=
  by
  suffices IsLeftRegular (X ^ n : R[X]) from ⟨this, this.right_of_commute (fun p => commute_X_pow p n)⟩
  intro P Q (hPQ : X ^ n * P = X ^ n * Q)
  ext i
  rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]

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