Additive submonoids of semirings

The binomial theorem gives a criterion for a power of a sum to lie in an additive submonoid: it suffices that every product of powers in the expansion belongs to the submonoid. This applies to additive subgroups as well, without requiring multiplicative closure.

theorem Commute.add_pow_mem_of_mul_pow_mem {R : Type u_1} {S : Type u_2} [Semiring R] [SetLike S R] [AddSubmonoidClass S R] {G : S} {a b : R} (hab : Commute a b) {n : ℕ} (h : ∀ k ≤ n, a ^ k * b ^ (n - k) ∈ G) : (a + b) ^ n ∈ G

If every product a ^ k * b ^ (n - k) lies in an additive submonoid and a commutes with b, then (a + b) ^ n lies in the submonoid.