mem_ker_truncate — Mathlib

English

An element x lies in the kernel of truncate n iff all its first n coefficients vanish: x ∈ ker(truncate n) ⇔ ∀ i < n, x.coeff i = 0.

Русский

Элемент x лежит в ядре усечения, если первые n коэффициентов равны нулю: x ∈ ker(truncate n) ⇔ ∀ i < n, x.coeff i = 0.

LaTeX

$$$$ x \\in \\ker(\\operatorname{truncate} (p := p) n) \\iff \\forall i < n, x.\\mathrm{coeff} i = 0. $$$$

Lean4

theorem mem_ker_truncate (x : 𝕎 R) : x ∈ RingHom.ker (truncate (p := p) n) ↔ ∀ i < n, x.coeff i = 0 :=
  by
  simp only [RingHom.mem_ker, truncate, RingHom.coe_mk, TruncatedWittVector.ext_iff, coeff_zero]
  exact Fin.forall_iff

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