subtype_injective

Mathlib.Algebra.Ring.Subring.Defs

URI: https://scilib.ai/kg/mathlib#Subring.subtype_injective

English

Let S be a subring of R. The natural inclusion map i: S → R is injective.

Русский

Пусть S является подкольцом R. Естественное включение i: S → R инъективно.

LaTeX

$$$\operatorname{Injective}(i)$ with $i:S\to R$, $i(s)=s$ for all $s\in S$.$$

Lean4

theorem subtype_injective (s : Subring R) : Function.Injective s.subtype :=
  s.toSubmonoid.subtype_injective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru