English
A type with multiplication and 1 is a right-cancel monoid if there exists an injective map to a right-cancel monoid preserving 1 and multiplication, and power structure is preserved.
Русский
Тип с умножением и единицей считается правок отменяемым моною, если существует инъективное отображение в правый отменяемый моноид, сохраняющее 1, умножение и степени.
LaTeX
$$$$ \\text{If } f: M_1 \\to M_2 \\text{ is injective and preserves } 1, * , \\text{ and } M_2 \\text{ is RightCancelMonoid}, \\text{ then } M_1 \\text{ is RightCancelMonoid.} $$$$
Lean4
/-- A type endowed with `1` and `*` is a right cancel monoid, if it admits an injective map that
preserves `1` and `*` to a right cancel monoid. See note [reducible non-instances]. -/
@[to_additive /-- A type endowed with `0` and `+` is an additive left cancel monoid,if it
admits an injective map that preserves `0` and `+` to an additive left cancel monoid. -/
]
protected abbrev rightCancelMonoid [RightCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1)
(mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : RightCancelMonoid M₁ :=
{ hf.rightCancelSemigroup f mul, hf.monoid f one mul npow with }
