charP_of_isFractionRing

Mathlib.Algebra.CharP.Algebra

URI: https://scilib.ai/kg/mathlib#IsFractionRing.charP_of_isFractionRing

← MathLib Explorer

English

If R has CharP p, then CharP(K) p for K = Frac(R).

Русский

Если R имеет CharP p, тогда CharP(p) у полей дробей Frac(R).

LaTeX

$$$( \\CharP(R,p) ) \\Rightarrow \\CharP(K,p)$$$

Lean4

/-- If `R` has characteristic `p`, then so does Frac(R). -/
theorem charP_of_isFractionRing [CharP R p] : CharP K p :=
  charP_of_injective_algebraMap (IsFractionRing.injective R K) p

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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