English
Let R be a semiring and X the formal indeterminate. Then for every n ∈ N, the truncation of X at level n+2 equals X.
Русский
Пусть R — полупрямое кольцо и X — формальный индетерминант. Тогда для каждого n ∈ N усечение X на уровне n+2 равно X.
LaTeX
$$$\\forall R [\\text{Semiring } R] \\; (\\forall n \\in \\mathbb{N}), \\; \\operatorname{trunc}(n+2) X = X$$$
Lean4
@[simp]
theorem trunc_X (n) : trunc (n + 2) X = (Polynomial.X : R[X]) :=
by
ext d
rw [coeff_trunc, coeff_X]
split_ifs with h₁ h₂
· rw [h₂, coeff_X_one]
· rw [coeff_X_of_ne_one h₂]
· rw [coeff_X_of_ne_one]
intro hd
apply h₁
rw [hd]
exact n.one_lt_succ_succ