instRightCommutativeOfCommutativeOfAssociative

English

If a binary operation f is commutative and associative, then f is right-commutative.

Русский

Если бинарная операция f коммутативна и ассоциативна, то она правокоммутативна.

LaTeX

$$$\\operatorname{Commutative}(f) \\land \\operatorname{Associative}(f) \\Rightarrow \\operatorname{RightCommutative}(f)$$$

Lean4

instance {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : RightCommutative f :=
  ⟨fun a b c ↦ by rw [ha.assoc, hc.comm b, ha.assoc]⟩

Похожие утверждения