Characteristic of subrings

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

Equations

• (_ : CharP (↥S) p) = (_ : CharP (↥S) p)

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

Equations

• (_ : CharP (↥S) p) = (_ : CharP (↥S) p)

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

Equations

• (_ : CharP (↥S) p) = (_ : CharP (↥S) p)