truncate_wittVector_truncate — Mathlib

English

The equality (truncate hm) ∘ WittVector.truncate m = WittVector.truncate n holds in the sense of function equality after applying coefficients.

Русский

Равенство (truncate hm) ∘ WittVector.truncate m = WittVector.truncate n верно в смысле равенства функций через коэффициенты.

LaTeX

$$$$ (\\operatorname{truncate} hm) \\circ (\\mathrm{WittVector.truncate} m) = \\mathrm{WittVector.truncate} n. $$$$

Lean4

@[simp]
theorem truncate_wittVector_truncate {m : ℕ} (hm : n ≤ m) (x : 𝕎 R) :
    truncate hm (WittVector.truncate m x) = WittVector.truncate n x :=
  RingHom.liftOfRightInverse_comp_apply _ _ _ _ _

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