trunc_X — Mathlib

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

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