charP — Mathlib

English

If R has characteristic p, then the fraction ring Frac(R) has characteristic p as well.

Русский

Если у кольца R характеристика p, то характеристика дробной кольца Frac(R) тоже равна p.

LaTeX

$$$ CharP\ R\ p \Rightarrow CharP\ (FractionRing\ R)\ p $$$

Lean4

/-- If `R` has characteristic `p`, then so does `FractionRing R`. -/
instance charP [CharP R p] : CharP (FractionRing R) p :=
  charP_of_isFractionRing R p

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