mulLeftEmbedding

Mathlib.Algebra.Group.Embedding

URI: https://scilib.ai/kg/mathlib#mulLeftEmbedding

Lean4

/-- If left-multiplication by any element is cancellative, left-multiplication by `g` is an
embedding. -/
@[to_additive (attr := simps (attr := grind =)) /--
    If left-addition by any element is cancellative, left-addition by `g` is an embedding. -/
    ]
def mulLeftEmbedding [Mul G] [IsLeftCancelMul G] (g : G) : G ↪ G
    where
  toFun h := g * h
  inj' := mul_right_injective g

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

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

Разделы

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

Аффилиация

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