Characteristic of subrings #
instance
CharP.subsemiring
(R : Type u)
[Semiring R]
(p : ℕ)
[CharP R p]
(S : Subsemiring R)
:
CharP (↥S) p
Equations
- ⋯ = ⋯
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