inclusion — Mathlib

English

Let S ⊆ T be subfields of a division ring K. The inclusion map i: S → T sending each element to itself is a ring homomorphism.

Русский

Пусть S ⊆ T — подполя поля K. Включение i: S → T, отображающее каждый элемент в самого себя, является кольцевым гомоморфизмом.

LaTeX

$$$ S \\le T \\Rightarrow i: S \\to+* T \\text{ is a ring homomorphism}$$$

Lean4

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

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