closureEquivAdjoinInt — Mathlib

English

For any ring R and subset s ⊆ R, there exists a canonical ℤ-algebra isomorphism between Subring.closure s and Algebra.adjoin ℤ s, given by the identity.

Русский

Пусть R — кольцо, s ⊆ R. Существует каноническое ℤ-алгебраическое изоморождение между Subring.closure s и Algebra.adjoin ℤ s, задаваемое тождеством.

LaTeX

$$\operatorname{Subring.closure}(s) \cong_{\mathbb{Z}} \operatorname{Algebra.adjoin}_{\mathbb{Z}} s$$

Lean4

/-- The `ℤ`-algebra equivalence between `Subring.closure s` and `Algebra.adjoin ℤ s` given by
the identity map. -/
def closureEquivAdjoinInt {R : Type*} [Ring R] (s : Set R) : Subring.closure s ≃ₐ[ℤ] Algebra.adjoin ℤ s :=
  Subalgebra.equivOfEq (subalgebraOfSubring <| Subring.closure s) _ (adjoin_int s).symm

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