truncate_comp_wittVector_truncate

English

For hm: n ≤ m, (truncate hm) ∘ (WittVector.truncate m) = WittVector.truncate n.

Русский

Для hm: n ≤ m, (truncate hm) ∘ (WittVector.truncate m) = WittVector.truncate n.

LaTeX

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

Lean4

@[simp]
theorem truncate_comp_wittVector_truncate {m : ℕ} (hm : n ≤ m) :
    (truncate (p := p) (R := R) hm).comp (WittVector.truncate m) = WittVector.truncate n :=
  RingHom.liftOfRightInverse_comp _ _ _ _

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