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