English
The compositions toPadicInt ∘ fromPadicInt and fromPadicInt ∘ toPadicInt are the identity on the appropriate domains.
Русский
Составы toPadicInt ∘ fromPadicInt и fromPadicInt ∘ toPadicInt являются тождественны на соответствующих областях.
LaTeX
$$$$ (toPadicInt\ p).\comb (fromPadicInt\ p) = \mathrm{id}_{\mathbb{Z}_{(p)}} , \quad (fromPadicInt\ p).\comb (toPadicInt\ p) = \mathrm{id}_{\mathbb{W}_p(\mathbb{Z}/p\mathbb{Z})}. $$$$
Lean4
theorem toPadicInt_comp_fromPadicInt : (toPadicInt p).comp (fromPadicInt p) = RingHom.id ℤ_[p] :=
by
rw [← PadicInt.toZModPow_eq_iff_ext]
intro n
rw [← RingHom.comp_assoc, toPadicInt, PadicInt.lift_spec]
simp only [fromPadicInt, toZModPow, RingHom.comp_id]
rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]
simp only [RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp]
