English
If f: M1 → M2 preserves multiplication and is injective, and M2 is left-cancellative, then M1 is left-cancellative.
Русский
Если существует инъективное отображение, сохраняющее произведение, и у M2 слева_cancel, то и у M1 левое-cancel.
LaTeX
$$$$ \\text{If } f: M_1 \\to M_2 \\text{ is injective and } (\\forall x,y, f(xy)=f(x)f(y)), \\text{ and } M_2 \\text{ is left-cancel}, \\text{ then } M_1 \\text{ is left-cancel.} $$$$
Lean4
/-- A type has left-cancellative multiplication, if it admits an injective map that
preserves `*` to another type with left-cancellative multiplication. -/
@[to_additive /-- A type has left-cancellative addition, if it admits an injective map that
preserves `+` to another type with left-cancellative addition. -/
]
protected theorem isLeftCancelMul [Mul M₂] [IsLeftCancelMul M₂] (f : M₁ → M₂) (hf : Injective f)
(mul : ∀ x y, f (x * y) = f x * f y) : IsLeftCancelMul M₁ where
mul_left_cancel x y z H := hf <| mul_left_cancel <| by simpa only [mul] using congrArg f H
