toLeftCancelMonoid_injective

Mathlib.Algebra.Group.Ext

URI: https://scilib.ai/kg/mathlib#CancelMonoid.toLeftCancelMonoid_injective

← MathLib Explorer

English

The map from LeftCancelMonoid to Monoid is injective.

Русский

Отображение из LeftCancelMonoid в Monoid инъективно.

LaTeX

$$$\text{toMonoid}$ is injective for LeftCancelMonoid structures: if two such structures map to the same monoid, they are equal.$$

Lean4

@[to_additive]
theorem toLeftCancelMonoid_injective {M : Type u} : Function.Injective (@CancelMonoid.toLeftCancelMonoid M) :=
  by
  rintro ⟨⟩ ⟨⟩ h
  congr

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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