truncateFun_pow — Mathlib

English

Let x be a Witt vector over R and m a natural number. Then truncation to the first n components preserves powers: truncateFun n (x ^ m) = truncateFun n x ^ m.

Русский

Пусть x — виттовектор над R и m натуральное. Тогда усечение до первых n координат сохраняет степени: truncateFun n (x^m) = (truncateFun n x)^m.

LaTeX

$$$$\\operatorname{truncateFun}_n(x^m) = (\\operatorname{truncateFun}_n x)^m.$$$$

Lean4

theorem truncateFun_pow (x : 𝕎 R) (m : ℕ) : truncateFun n (x ^ m) = truncateFun n x ^ m := by witt_truncateFun_tac

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