English
In a commutative magma, right cancellation implies full cancellation (i.e. both left and right cancel).
Русский
В коммутативной магме правое отменение влечет за собой полное отменение (то есть и слева, и справа отменяются).
LaTeX
$$$\\forall G\\, (\\text{CommMagma } G)\\;\\&\\; (\\text{IsRightCancelMul } G) \\Rightarrow (\\text{IsCancelMul } G).$$$
Lean4
/-- Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsCancelMul G`. -/
@[to_additive AddCommMagma.IsRightCancelAdd.toIsCancelAdd /-- Any `AddCommMagma G` that satisfies
`IsRightCancelAdd G` also satisfies `IsCancelAdd G`. -/
]
theorem toIsCancelMul (G : Type u) [CommMagma G] [IsRightCancelMul G] : IsCancelMul G :=
{ CommMagma.IsRightCancelMul.toIsLeftCancelMul G with }
