pthRoot_frobenius — Mathlib

English

The p-th root map and Frobenius operator compose to identity on the perfection: pthRoot R p ∘ frobenius_p = id.

Русский

Порядок p-й корень и Фробениус образуют тождественный отображение на перфекции: pthRoot R p ∘ frobenius_p = id.

LaTeX

$$$(\\mathrm{pthRoot} \\; R \\; p) \\circ (\\mathrm{frobenius}_{p}) = \\mathrm{id}_{\\mathrm{Ring.Perfection}(R,p)}$$$

Lean4

theorem pthRoot_frobenius : (pthRoot R p).comp (frobenius _ p) = RingHom.id _ :=
  RingHom.ext fun x => ext fun n => by rw [RingHom.comp_apply, RingHom.id_apply, coeff_pthRoot, coeff_frobenius]

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