Characteristic of subrings

instance CharP.subsemiring (R : Type u) [Semiring R] (p : ℕ) [CharP R p] (S : Subsemiring R) : CharP (↥S) p

instance CharP.subring (R : Type u) [Ring R] (p : ℕ) [CharP R p] (S : Subring R) : CharP (↥S) p

instance CharP.subring' (R : Type u) [CommRing R] (p : ℕ) [CharP R p] (S : Subring R) : CharP (↥S) p

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

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