English
Let R, S be rings and s ≤ R a subring. If f: R →+* S is injective, then the subring s is isomorphic to its image s.map f under the restriction of f to s; i.e., there exists a ring isomorphism between s and s.map f.
Русский
Пусть R, S — кольца, s ≤ R — подкольцо. Пусть f: R →+* S инъективен. Тогда подкольцо s изоморфно своему образу s.map f через ограничение f на s; существует кольцевое изоморфизм между s и s.map f.
LaTeX
$$$\\exists \\phi:\\; s \\cong+* s.map f$$$
Lean4
/-- A subring is isomorphic to its image under an injective function -/
noncomputable def equivMapOfInjective (f : R →+* S) (hf : Function.Injective f) : s ≃+* s.map f :=
{ Equiv.Set.image f s hf with
map_mul' := fun _ _ => Subtype.ext (f.map_mul _ _)
map_add' := fun _ _ => Subtype.ext (f.map_add _ _) }
