sumCongr_mul — Mathlib

English

For e,f,g,h ∈ Perm α, Perm β, the block permutation sumCongr e f and sumCongr g h multiplies to sumCongr (e g) (f h).

Русский

Для e,f ∈ Perm α и g,h ∈ Perm β произведение суммирующей перестановки равно сумме перестановок: (sumCongr e f)(sumCongr g h) = sumCongr (e g) (f h).

LaTeX

$$$$(sumCongr\, e\, f) \\, (sumCongr\, g\, h) = sumCongr (e g) (f h).$$$$

Lean4

@[simp]
theorem sumCongr_mul {α β : Type*} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β) :
    sumCongr e f * sumCongr g h = sumCongr (e * g) (f * h) :=
  sumCongr_trans g h e f

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