truncateFun_out — Mathlib

English

For every x in TruncatedWittVector p n R, applying out to x and then truncateFun recovers x: truncateFun(n)(x.out) = x.

Русский

Для любого x из TruncatedWittVector p n R применение out к x, затем усечение восстанавливает x: truncateFun(n)(x.out) = x.

LaTeX

$$$ \operatorname{truncateFun}(n)(x.\mathrm{out}) = x $$$

Lean4

@[simp]
theorem truncateFun_out (x : TruncatedWittVector p n R) : x.out.truncateFun n = x := by
  simp only [WittVector.truncateFun, coeff_out, mk_coeff]

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