Characteristic of subrings #
instance
CharP.subsemiring
(R : Type u)
[Semiring R]
(p : ℕ)
[CharP R p]
(S : Subsemiring R)
:
CharP (↥S) p
The characteristic of a division ring is equal to the characteristic of its center
The characteristic of a division ring is equal to the characteristic of its center