perfectRing — Mathlib

English

The ring Ring.Perfection R p is perfect of characteristic p; that is, it has bijective Frobenius.

Русский

Кольцо Ring.Perfection R p является совершенным кольцом характерности p, т.е. у него биективный Фробениус.

LaTeX

$$PerfectRing (Ring.Perfection R p) p$$

Lean4

instance perfectRing : PerfectRing (Ring.Perfection R p) p where
  bijective_frobenius :=
    Function.bijective_iff_has_inverse.mpr
      ⟨pthRoot R p, DFunLike.congr_fun <| @frobenius_pthRoot R _ p _ _,
        DFunLike.congr_fun <| @pthRoot_frobenius R _ p _ _⟩

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