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