toAddSubmonoid_injective

Mathlib.Algebra.Ring.Subsemiring.Defs

URI: https://scilib.ai/kg/mathlib#Subsemiring.toAddSubmonoid_injective

English

The map toAddSubmonoid: Subsemiring R → AddSubmonoid R is injective.

Русский

Вобраз toAddSubmonoid: Subsemiring R → AddSubmonoid R инъективно.

LaTeX

$$Injective (toAddSubmonoid : Subsemiring R → AddSubmonoid R)$$

Lean4

theorem toAddSubmonoid_injective : Function.Injective (toAddSubmonoid : Subsemiring R → AddSubmonoid R)
  | _, _, h => ext (SetLike.ext_iff.mp h :)

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

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

Разделы

Аффилиация

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