closureEquivAdjoinNat — Mathlib

English

Let s be a subset of a semiring R. Then Subsemiring.closure s and Algebra.adjoin ℕ s are canonically isomorphic as ℕ-algebras, via the identity map.

Русский

Пусть s ⊆ R и R — полусемiring. Тогда Subsemiring.closure s и Algebra.adjoin ℕ s канонически изоморфны как ℕ-алгебры, тождественным отображением.

LaTeX

$$\operatorname{Subsemiring.closure}(s) \cong_{\mathbb{N}} \operatorname{Algebra.adjoin}_{\mathbb{N}} s$$

Lean4

/-- The `ℕ`-algebra equivalence between `Subsemiring.closure s` and `Algebra.adjoin ℕ s` given
by the identity map. -/
def closureEquivAdjoinNat {R : Type*} [Semiring R] (s : Set R) : Subsemiring.closure s ≃ₐ[ℕ] Algebra.adjoin ℕ s :=
  Subalgebra.equivOfEq (subalgebraOfSubsemiring <| Subsemiring.closure s) _ (adjoin_nat s).symm

Похожие утверждения