English
Let G be a commutative magma with the binary operation ·. If right cancellation holds, i.e. a·b = a·c implies b = c for all a,b,c ∈ G, then left cancellation also holds, i.e. b·a = c·a implies b = c for all a,b,c ∈ G.
Русский
Пусть G — коммутативная магма с бинарной операцией ·. Если выполняется правое отменение: для любых a,b,c ∈ G, a·b = a·c ⇒ b = c, то выполняется и левое отменение: для любых a,b,c ∈ G, b·a = c·a ⇒ b = c.
LaTeX
$$$\\forall G\\, (\\text{CommMagma } G) \\;\\Rightarrow\\; (\\forall a,b,c \\in G\\, (a \\cdot b = a \\cdot c \\Rightarrow b=c)) \\Rightarrow (\\forall a,b,c \\in G\\, (b \\cdot a = c \\cdot a \\Rightarrow b=c)).$$$
Lean4
/-- Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsLeftCancelMul G`. -/
@[to_additive AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd /-- Any `AddCommMagma G` that
satisfies `IsRightCancelAdd G` also satisfies `IsLeftCancelAdd G`. -/
]
theorem toIsLeftCancelMul (G : Type u) [CommMagma G] [IsRightCancelMul G] : IsLeftCancelMul G :=
⟨fun _ _ _ h => mul_right_cancel <| (mul_comm _ _).trans (h.trans (mul_comm _ _))⟩
