truncate_surjective — Mathlib

English

The truncation map truncate n: 𝕎 R → TruncatedWittVector p n R is surjective for hm: n ≤ m.

Русский

Ограничение усечения truncate n: 𝕎 R → TruncatedWittVector p n R является сюръективным при hm: n ≤ m.

LaTeX

$$$$\\operatorname{truncate}_{n}: \\mathbb{W}R \\to \\mathrm{TruncatedWittVector}_{p}^{\,n}R \\text{ is surjective}. $$$$

Lean4

theorem truncate_surjective : Surjective (truncate n : 𝕎 R → TruncatedWittVector p n R) :=
  truncateFun_surjective p n R

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