trunc_X_of — Mathlib

English

Let R be a semiring and X the indeterminate. If 2 ≤ n, then trunc n X = X.

Русский

Пусть R — полупрямое кольцо и X — индетерминант. Если 2 ≤ n, то trunc n X = X.

LaTeX

$$$\\forall R [\\text{Semiring } R] \\; (n : \\mathbb{N}), \\; 2 \\le n \\Rightarrow \\operatorname{trunc} n X = X$$$

Lean4

theorem trunc_X_of {n : ℕ} (hn : 2 ≤ n) : trunc n X = (Polynomial.X : R[X]) := by
  cases n with
  | zero => contradiction
  | succ n =>
    cases n with
    | zero => contradiction
    | succ n => exact trunc_X n

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