English
For a set s in a semiring R, adjoinNat s equals the subalgebra of Subsemiring closure, i.e., adjoin with Nat equals the subalgebra generated by the semiring closure of s.
Русский
Для множества s в полукольце R, adjoin Nat s равен подалгебре, порождённой замыканием полусемиринга Subsemiring.closure s.
LaTeX
$$$\\operatorname{adjoin}_{\\mathbb{N}} s = \\operatorname{subalgebraOfSubsemiring}(\\operatorname{Subsemiring.closure} s)$$$
Lean4
theorem adjoin_nat {R : Type*} [Semiring R] (s : Set R) :
adjoin ℕ s = subalgebraOfSubsemiring (Subsemiring.closure s) :=
le_antisymm (adjoin_le Subsemiring.subset_closure)
(Subsemiring.closure_le.2 subset_adjoin : Subsemiring.closure s ≤ (adjoin ℕ s).toSubsemiring)
