subring — Mathlib

English

The characteristic of the center of a ring equals the characteristic of the ring itself.

Русский

Характеристика центра кольца равна характеристике самого кольца.

LaTeX

$$$\\mathrm{CharP}(\\mathrm{Subring.center}\n R)\\, p \\iff \\mathrm{CharP}(R)\\, p$$$

Lean4

instance subring (R : Type u) [Ring R] (p : ℕ) [CharP R p] (S : Subring R) : CharP S p :=
  ⟨fun x =>
    Iff.symm <|
      (CharP.cast_eq_zero_iff R p x).symm.trans
        ⟨fun h => Subtype.eq <| show S.subtype x = 0 by rw [map_natCast, h], fun h =>
          map_natCast S.subtype x ▸ by rw [h, RingHom.map_zero]⟩⟩

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