fromPadicInt_comp_toPadicInt — Mathlib

English

The extension lemma for fromPadicInt and toPadicInt identities.

Русский

Лемма расширения для fromPadicInt и toPadicInt.

LaTeX

$$$$ \text{fromPadicInt} \circ \text{toPadicInt} = \mathrm{id} \quad \text{and} \; \text{toPadicInt} \circ \text{fromPadicInt} = \mathrm{id}. $$$$

Lean4

theorem fromPadicInt_comp_toPadicInt : (fromPadicInt p).comp (toPadicInt p) = RingHom.id (𝕎 (ZMod p)) :=
  by
  apply WittVector.hom_ext
  intro n
  rw [fromPadicInt, ← RingHom.comp_assoc, truncate_comp_lift, RingHom.comp_assoc]
  simp only [toPadicInt, toZModPow, RingHom.comp_id, PadicInt.lift_spec, RingHom.id_comp, ← RingHom.comp_assoc,
    RingEquiv.toRingHom_comp_symm_toRingHom]

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