English
The underlying subring of the adjoin is the ring-closure of the algebra map range together with s: (adjoin_R s).toSubring = Subring.closure(range(algebraMap R A) ∪ s).
Русский
Базовый подкольцо adjoin_R s равно замыканию кольца над образами algebraMap_R и множества s.
LaTeX
$$$(\\operatorname{adjoin}_R s).toSubring = \\operatorname{Subring.closure}(\\operatorname{range}(\\operatorname{algebraMap} R A) \\cup s)$$$
Lean4
theorem adjoin_eq_ring_closure (s : Set A) :
(adjoin R s).toSubring = Subring.closure (Set.range (algebraMap R A) ∪ s) :=
.symm <|
Subring.closure_eq_of_le (by simp [adjoin]) fun x hx =>
Subsemiring.closure_induction Subring.subset_closure (Subring.zero_mem _) (Subring.one_mem _)
(fun _ _ _ _ => Subring.add_mem _) (fun _ _ _ _ => Subring.mul_mem _) hx
