sumSumSumComm_symm — Mathlib

English

(sumSumSumComm α β γ δ).symm = sumSumSumComm α γ β δ.

Русский

Симметрия четырехразовой суммы: обратное к преобразованию равно преобразованию с swapped β и γ.

LaTeX

$$$$(\mathrm{sumSumSumComm}(\alpha,\beta,\gamma,\delta))^{-1} = \mathrm{sumSumSumComm}(\alpha,\gamma,\beta,\delta).$$$$

Lean4

@[simp]
theorem sumSumSumComm_symm (α β γ δ) : (sumSumSumComm α β γ δ).symm = sumSumSumComm α γ β δ :=
  rfl

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