out_injective — Mathlib

English

The truncation map from truncated Witt vectors to Witt vectors is injective: if out x = out y, then x = y for all p, n, and R (with R a commutative ring).

Русский

Обособленное отображение усечения от обрезанных виттовых векторов к виттовым векторам инъективно: если out x = out y, то x = y, для любых p, n и кольца R, коммутативного по умолчанию.

LaTeX

$$$\forall x,y:\n\mathrm{TruncatedWittVector}(p,n,R),\; \mathrm{out}(x)=\mathrm{out}(y) \Rightarrow x=y$$$

Lean4

theorem out_injective : Injective (@out p n R _) := by
  intro x y h
  ext i
  rw [WittVector.ext_iff] at h
  simpa only [coeff_out] using h ↑i

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