inclusion — Mathlib

English

If S and T are subrings of R with S ≤ T, then the inclusion map S → T is a ring homomorphism.

Русский

Если S и T — подкольца R и S ⊆ T, то включение S → T является гомоморфизмом колец.

LaTeX

$$$ \\iota : S \\to T \\text{ есть кольцевой гомоморфизм, если } S \\le T $$$

Lean4

/-- The ring homomorphism associated to an inclusion of subrings. -/
def inclusion {S T : Subring R} (h : S ≤ T) : S →+* T :=
  S.subtype.codRestrict _ fun x => h x.2

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