not_isUnit_X_pow_sub_one — Mathlib

English

For a nontrivial ring R, X^n − 1 is not a unit for any n.

Русский

В не тривиальном кольце R элемент X^n − 1 не является единицей для любого n.

LaTeX

$$$\forall R [\text{Ring } R] [\text{Nontrivial } R] \forall n : \mathbb{N}, \neg IsUnit\left(X^n - 1 : R[X]\right)$$$

Lean4

theorem not_isUnit_X_pow_sub_one (R : Type*) [Ring R] [Nontrivial R] (n : ℕ) : ¬IsUnit (X ^ n - 1 : R[X]) :=
  by
  intro h
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp at h
  apply hn
  rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]

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