English
Let e: α ≃ β. If β has a multiplication and the left-cancellation property IsCancelMul β, then α, with the transported multiplication, also satisfies IsCancelMul α.
Русский
Пусть e: α ≃ β. Если β имеет умножение и выполняется свойство левого отмена IsCancelMul β, то α, с перенесённым по e умножением, тоже удовлетворяет IsCancelMul α.
LaTeX
$$$\forall a,b,c \in \alpha\; e^{-1}(e(a)\cdot e(b)) = e^{-1}(e(a)\cdot e(c)) \Rightarrow b=c$$$
Lean4
/-- Transfer `IsCancelMul` across an `Equiv` -/
@[to_additive /-- Transfer `IsCancelAdd` across an `Equiv` -/
]
protected theorem isCancelMul [Mul β] [IsCancelMul β] :
letI := e.mul
IsCancelMul α :=
by letI := e.mul; exact e.injective.isCancelMul _ fun _ _ ↦ e.apply_symm_apply _
