English
Let S be a nonunital subsemiring of R. Then there is a nonunital ℕ-subalgebra of R whose underlying nonunital subsemiring is S, with the ℕ-action given by the natural ℕ-multiplication (n • x equals the sum of x with itself n times).
Русский
Пусть S — неединичная подпполоска R. Тогда существует неединичная ℕ-подалгебра над R, бинтивно имеющая носитель S и действие ℕ на S, заданное натуральным умножением: n • x — это сумма x самого себя n раз.
LaTeX
$$$\\text{Given } S \\le R \\text{ a nonunital subsemiring, there is a nonunital }\\mathbb{N}\\text{-subalgebra of } R\\text{ with carrier }S\\text{ and }n\\cdot x\\in S\\text{ for all }n\\in\\mathbb{N}, x\\in S,$$$
Lean4
/-- A non-unital subsemiring is a non-unital `ℕ`-subalgebra. -/
def nonUnitalSubalgebraOfNonUnitalSubsemiring (S : NonUnitalSubsemiring R) : NonUnitalSubalgebra ℕ R
where
toNonUnitalSubsemiring := S
smul_mem' n _x hx := nsmul_mem (S := S) hx n
