Characteristic of subrings

theorem SubsemiringClass.charP_iff {R : Type u} {S : Type v} [SetLike S R] [NonAssocSemiring R] [SubsemiringClass S R] {p : ℕ} {s : S} : CharP (↥s) p ↔ CharP R p

@[deprecated SubsemiringClass.charP_iff (since := "2026-10-15")]

theorem CharP.charP_center_iff {R : Type u} [Ring R] {p : ℕ} : CharP (↥(Subring.center R)) p ↔ CharP R p

The characteristic of a division ring is equal to the characteristic of its center

instance instCharPSubtypeMem {R : Type u} {S : Type v} [SetLike S R] [NonAssocSemiring R] [SubsemiringClass S R] {p : ℕ} [CharP R p] (s : S) : CharP (↥s) p

theorem SubsemiringClass.expChar_iff {R : Type u} {S : Type v} [SetLike S R] [NonAssocSemiring R] [SubsemiringClass S R] {p : ℕ} {s : S} : ExpChar (↥s) p ↔ ExpChar R p

@[deprecated SubsemiringClass.expChar_iff (since := "2026-10-15")]

theorem ExpChar.expChar_center_iff {R : Type u} [Ring R] {p : ℕ} : ExpChar (↥(Subring.center R)) p ↔ ExpChar R p

instance instExpCharSubtypeMem {R : Type u} {S : Type v} [SetLike S R] [NonAssocSemiring R] [SubsemiringClass S R] {p : ℕ} [ExpChar R p] (s : S) : ExpChar (↥s) p