commRing

Mathlib.RingTheory.Perfection

URI: https://scilib.ai/kg/mathlib#Perfection.commRing

English

If R is a commutative ring with characteristic p, then Ring.Perfection(R,p) is a commutative ring.

Русский

Если R — коммутативное кольцо с характеристикой p, то Ring.Perfection(R,p) — коммутативное кольцо.

LaTeX

$$Perfection.commRing(R,p)$$

Lean4

instance commRing (R : Type u₁) [CommRing R] [CharP R p] : CommRing (Ring.Perfection R p) :=
  (Ring.perfectionSubring R p).toCommRing

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru