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