left_comm — Mathlib

English

If a is central, then a commutes with the product of b and c on the left: a · (b · c) = b · (a · c).

Русский

Если a центральен, то a коммутирует с произведением b и c слева: a · (b · c) = b · (a · c).

LaTeX

$$$a * (b * c) = b * (a * c)$$$

Lean4

@[to_additive]
protected theorem left_comm (h : IsMulCentral a) (b c) : a * (b * c) = b * (a * c) := by
  simp only [(h.comm _).eq, h.right_assoc]
    -- cf. `Commute.right_comm`

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