ofFiniteOfIsReduced — Mathlib

English

If R is a finite, reduced ring with characteristic p, then R is a perfect ring of characteristic p.

Русский

Если R — конечное редуцированное кольцо характеристик p, то R совершенное по p.

LaTeX

$$Finite(R) ∧ IsReduced(R) ⇒ PerfectRing(R,p)$$

Lean4

instance ofFiniteOfIsReduced (R : Type*) [CommRing R] [ExpChar R p] [Finite R] [IsReduced R] : PerfectRing R p :=
  ofSurjective _ _ <| Finite.surjective_of_injective (frobenius_inj R p)

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