English
The left-cancellation property transfers along an equivalence: if β is left-cancelable, then α is left-cancelable under the transported multiplication.
Русский
Свойство левого отменяющего умножения переносится через эквивалент: если β слева отменимо, то α тоже будет слева отменяемым под переносимым умножением.
LaTeX
$$$$\text{If } (\forall a,b,c\in \alpha),\ a\cdot b = a\cdot c \Rightarrow b=c.$$$$
Lean4
/-- Transfer `IsLeftCancelMul` across an `Equiv` -/
@[to_additive /-- Transfer `IsLeftCancelAdd` across an `Equiv` -/
]
protected theorem isLeftCancelMul [Mul β] [IsLeftCancelMul β] :
letI := e.mul
IsLeftCancelMul α :=
by letI := e.mul; exact e.injective.isLeftCancelMul _ fun _ _ ↦ e.apply_symm_apply _
