Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem

theorem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (S' : Subalgebra R S) {ι : Type u_3} (ι' : Finset ι) (s l : ι → S), (ι'.sum fun i => l i * s i) = 1 → (∀ (i : ι), s i ∈ S') → (∀ (i : ι), l i ∈ S') → ∀ (x : S), (∀ (i : ι), ∃ n, s i ^ n • x ∈ S') → x ∈ S'

The theorem states that given a commutative semiring `R` and a commutative ring `S` in which `R` is an algebra over `S`, if we have a subalgebra `S'` of `S` and a finite set `ι'` such that the sum of the products of the elements `l i` and `s i` (for each `i` in `ι'`) equals 1, and each `s i` and `l i` is in `S'`, then an element `x` of `S` is in `S'` if and only if for each `i` in `ι'`, there exists a natural number `n` such that `s i` raised to the power `n` times `x` is in `S'`.

More concisely: Given a commutative semiring `R` being an algebra over a commutative ring `S`, a subalgebra `S'` of `S`, and a finite set `ι'` such that the products of `s i` and `l i` (for each `i` in `ι'`) sum to 1 with all `s i`, `l i` in `S'`, if an element `x` of `S` satisfies the power conditions `s i^n * x` in `S'` for each `i` and some natural number `n`, then `x` is in `S'`.