inclusion — Mathlib

English

The inclusion of a subsemiring S into T, when S ≤ T, is a ring homomorphism.

Русский

Включение S в T, если S ≤ T, является кольцевым гомоморфизмом.

LaTeX

$$$\\text{inclusion}_h : S \\to+* T$ is a ring homomorphism whenever $S \\le T$.$$

Lean4

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

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