comp_equiv' — Mathlib

English

For a perfection map m with π, the composition with the equivalence recovers π on x: coeff R p 0 (m.equiv x) = π x.

Русский

Для отображения m с π композиция восстанавливает π на x: coeff R p 0 (m.equiv x) = π x.

LaTeX

$$$\\operatorname{coeff} R p 0 (m.\\mathrm{equiv}\ x) = \\pi x$$$

Lean4

theorem comp_equiv' {π : P →+* R} (m : PerfectionMap p π) : (Perfection.coeff R p 0).comp ↑m.equiv = π :=
  RingHom.ext fun _ => rfl

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