truncateFun_surjective — Mathlib

English

The truncation map truncateFun is surjective: for every truncated Witt vector z, there exists x with truncateFun(n)(x) = z.

Русский

Отображение усечения surjective: для каждого усечённого виттового вектора z существует x такой, что truncateFun(n)(x) = z.

LaTeX

$$$ \mathrm{Surjective}(\mathrm{WittVector.truncateFun}\,n) $$$

Lean4

theorem truncateFun_surjective : Surjective (@truncateFun p n R) :=
  Function.RightInverse.surjective TruncatedWittVector.truncateFun_out

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