truncate_comp_lift — Mathlib

English

The composition of truncate n with WittVector.lift equals the original f: (WittVector.truncate n) ∘ (lift f_compat) = f n.

Русский

Составление truncate n с WittVector.lift даёт исходный f n: (truncate n) ∘ (lift f_compat) = f n.

LaTeX

$$$$ (\\operatorname{truncate} n) \\circ (\\mathrm{WittVector.lift} f f_{\\mathrm{compat}}) = f n. $$$$

Lean4

@[simp]
theorem truncate_comp_lift : (WittVector.truncate n).comp (lift _ f_compat) = f n := by ext1;
  rw [RingHom.comp_apply, truncate_lift]

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