mulRightEmbedding

Mathlib.Algebra.Group.Embedding

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

Lean4

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

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

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

Разделы

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

Аффилиация

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