inl_injective

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.inl_injective

English

The map inl: R → tsze R M is injective provided M is a zero object.

Русский

Отображение inl: R → tsze R M инъективно, если M имеет нулевой элемент.

LaTeX

$$inl: R → tsze R M инъективно$$

Lean4

theorem inl_injective [Zero M] : Function.Injective (inl : R → tsze R M) :=
  Function.LeftInverse.injective <| fst_inl _

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

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

Разделы

Аффилиация

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