English
If a type M1 injects into a monoid M2 preserving 1 and multiplication, then M1 inherits monoid structure from M2.
Русский
Если M1 инъективно внедряется в моноид M2, сохраняющий 1 и умножение, то M1 наследует структуру моноида от M2.
LaTeX
$$$$ \\text{If } f: M_1 \\to M_2 \\text{ is injective and preserves } 1, * , \\text{ then } M_1 \\text{ can be given a Monoid structure.} $$$$
Lean4
/-- A type endowed with `1` and `*` is a left cancel monoid, if it admits an injective map that
preserves `1` and `*` to a left 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 leftCancelMonoid [LeftCancelMonoid 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) : LeftCancelMonoid M₁ :=
{ hf.leftCancelSemigroup f mul, hf.monoid f one mul npow with }
