instLeftCommutativeOfCommutativeOfAssociative

English

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

Русский

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

LaTeX

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

Lean4

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

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