rightCancelSemigroup

Mathlib.Algebra.Group.InjSurj

URI: https://scilib.ai/kg/mathlib#Function.Injective.rightCancelSemigroup

Lean4

/-- A type endowed with `*` is a right cancel semigroup, if it admits an injective map that
preserves `*` to a right cancel semigroup.  See note [reducible non-instances]. -/
@[to_additive /-- A type endowed with `+` is an additive right
    cancel semigroup, if it admits an injective map that preserves `+` to an additive right cancel
    semigroup. -/
    ]
protected abbrev rightCancelSemigroup [RightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f)
    (mul : ∀ x y, f (x * y) = f x * f y) : RightCancelSemigroup M₁ :=
  { hf.semigroup f mul, hf.isRightCancelMul f mul with }

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

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

Разделы

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

Аффилиация

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