commSemiring

Mathlib.RingTheory.Perfection

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

English

If R has characteristic p and p is prime, then Ring.Perfection(R,p) also has characteristic p.

Русский

Если у R характеристика p и p простое, то у Ring.Perfection(R,p) также характеристика p.

LaTeX

$$CharP(Ring.Perfection(R,p), p)$$

Lean4

instance commSemiring : CommSemiring (Ring.Perfection R p) :=
  (Ring.perfectionSubsemiring R p).toCommSemiring

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

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

Разделы

Аффилиация

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