English
Let e be a type equivalence e: α ≃ β. If β carries a multiplication with the right-cancellation property, then α, equipped with the multiplication transported along e (a starred product a ∗ b := e⁻¹(e(a) · e(b))), also has the right-cancellation property.
Русский
Пусть e: α ≃ β. Если β имеет умножение с правым свойством отмены, то α, наделённый перенесённым по e умножением (a ∗ b := e⁻¹(e(a) · e(b))), также обладает правым свойством отмены.
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 `IsRightCancelMul` across an `Equiv` -/
@[to_additive /-- Transfer `IsRightCancelAdd` across an `Equiv` -/
]
protected theorem isRightCancelMul [Mul β] [IsRightCancelMul β] :
letI := e.mul
IsRightCancelMul α :=
by letI := e.mul; exact e.injective.isRightCancelMul _ fun _ _ ↦ e.apply_symm_apply _
