toMonoid_injective

Mathlib.Algebra.Group.Ext

URI: https://scilib.ai/kg/mathlib#LeftCancelMonoid.toMonoid_injective

← MathLib Explorer

English

Two LeftCancelMonoid structures are equal if their multiplications agree.

Русский

Две структуры LeftCancelMonoid равны, если их умножения совпадают.

LaTeX

$$$(\\forall x,y \in M), x *_{m_1} y = x *_{m_2} y \Rightarrow m_1 = m_2$$$

Lean4

@[to_additive]
theorem toMonoid_injective {M : Type u} : Function.Injective (@LeftCancelMonoid.toMonoid M) :=
  by
  rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h
  congr <;> injection h

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

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

Разделы

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

Аффилиация

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