comp_symm_equiv — Mathlib

English

For m: PerfectionMap p π, we have π (m.equiv.symm f) = Perfection.coeff R p 0 f.

Русский

Для m: PerfectionMap p π имеем π (m.equiv.symm f) = Perfection.coeff R p 0 f.

LaTeX

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

Lean4

theorem comp_symm_equiv {π : P →+* R} (m : PerfectionMap p π) (f : Ring.Perfection R p) :
    π (m.equiv.symm f) = Perfection.coeff R p 0 f :=
  (m.comp_equiv _).symm.trans <| congr_arg _ <| m.equiv.apply_symm_apply f

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