instance Subsingleton.charP (R : Type u_1) [AddMonoidWithOne R] [Subsingleton R] : CharP R 1

theorem Nontrivial.of_expChar (R : Type u_1) [AddMonoidWithOne R] (q : ℕ) [hq : ExpChar R q] : Nontrivial R

If R has an exponential characteristic, it is nontrivial.