sumCongr_symm — Mathlib

English

The symmetric of sumCongr equals the sumCongr of symmetric components for permutations.

Русский

Симметрическая части sumCongr равна sumCongr симметричных компонентов перестановок.

LaTeX

$$sumCongr_symm {α β} (e : Equiv.Perm α) (f : Equiv.Perm β) : (sumCongr e f).symm = sumCongr e.symm f.symm$$

Lean4

theorem sumCongr_symm {α β} (e : Equiv.Perm α) (f : Equiv.Perm β) : (sumCongr e f).symm = sumCongr e.symm f.symm :=
  Equiv.sumCongr_symm e f

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