charZero_of_isFractionRing — Mathlib

English

If R has characteristic zero, then its fraction ring (the field of fractions) has characteristic zero as well.

Русский

Если у кольца R характеристика ноль, то его кольцо дробей также имеет характеристику ноль.

LaTeX

$$$ CharZero\ R \Rightarrow CharZero\ K $$$

Lean4

/-- If `R` has characteristic `0`, then so does Frac(R). -/
theorem charZero_of_isFractionRing [CharZero R] : CharZero K :=
  @CharP.charP_to_charZero K _ (charP_of_isFractionRing R 0)

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