mul_right — Mathlib

English

If a commutes with both b and c, then a commutes with their product bc.

Русский

Если a коммутирует с b и с c, то a коммутирует с произведением bc.

LaTeX

$$$\\forall S [Semigroup S],\\ a,b,c \\in S,\\ Commute a b \\rightarrow Commute a c \\rightarrow Commute a (b c)$$$

Lean4

/-- If `a` commutes with both `b` and `c`, then it commutes with their product. -/
@[to_additive (attr := simp) /-- If `a` commutes with both `b` and `c`, then it commutes with their sum. -/
    ]
theorem mul_right (hab : Commute a b) (hac : Commute a c) : Commute a (b * c) :=
  SemiconjBy.mul_right hab hac

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