truncate_comp — Mathlib

English

For n1 ≤ n2 ≤ n3, the composition of truncated Witt vector truncations satisfies (truncate h1) ∘ (truncate h2) = truncate (h1.trans h2).

Русский

Для n1 ≤ n2 ≤ n3 композиция усечений виттового вектора удовлетворяет (truncate h1) ∘ (truncate h2) = truncate (h1.trans h2).

LaTeX

$$$$ (\\operatorname{truncate} (p := p) (R := R) h1).comp (\\operatorname{truncate} h2) = \\operatorname{truncate} (h1.trans h2). $$$$

Lean4

@[simp]
theorem truncate_comp {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃) :
    (truncate (p := p) (R := R) h1).comp (truncate h2) = truncate (h1.trans h2) := by ext1 x;
  simp only [truncate_truncate, Function.comp_apply, RingHom.coe_comp]

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