∀ (R : Type u_2) (A : Type u_1) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (p : ℕ)
  [ExpChar A p] {a b : A},
  a ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS} →
    b ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS} → a + b ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS}