mid_assoc — Mathlib

English

If z is central with respect to a, then for all a, c, a · z · c = a · (z · c).

Русский

Пусть z центрально для a; тогда для любых a, c выполняется a · z · c = a · (z · c).

LaTeX

$$$a \\cdot z \\cdot c = a \\cdot (z \\cdot c)$$$

Lean4

@[to_additive]
protected theorem mid_assoc {z : M} (h : IsMulCentral z) (a c) : a * z * c = a * (z * c) := by
  rw [h.comm, ← h.right_assoc, ← h.comm, ← h.left_assoc, h.comm]
    -- cf. `Commute.left_comm`

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