English
If there exists an injective map f from a type M1 with a unit and multiplication (and powers) into a cancellative monoid M2 that preserves 1, multiplication, and natural powers, then M1 inherits the cancellative monoid structure.
Русский
Пусть существует инъективное отображение f: M1 → M2 из множества M1, на котором определены единица и умножение (и степени), в отменяемый моноид M2, сохраняющее 1, умножение и степени натурального порядка; тогда M1 оказывается отменяемым моноидом.
LaTeX
$$$\exists f: M_1 \to M_2\,\big(\text{Injective}(f) \land f(1)=1 \land (\forall x,y: M_1)\, f(xy)=f(x)f(y) \land (\forall x: M_1)(\forall n:\mathbb{N})\, f(x^n)=f(x)^n\big)\land \text{CancelMonoid}(M_2) \Rightarrow \text{CancelMonoid}(M_1)$$
Lean4
/-- A type endowed with `1` and `*` is a cancel monoid, if it admits an injective map that preserves
`1` and `*` to a 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 cancelMonoid [CancelMonoid 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) : CancelMonoid M₁ :=
{ hf.leftCancelMonoid f one mul npow, hf.rightCancelMonoid f one mul npow with }
