permCongr_mul — Mathlib

English

Conjugation respects multiplication: e.permCongr(p q) = e.permCongr(p) · e.permCongr(q).

Русский

Сопряжение сохраняет умножение: e.permCongr(p q) = e.permCongr(p) · e.permCongr(q).

LaTeX

$$$$ e.\mathrm{permCongr}(p q) = e.\mathrm{permCongr}(p) \cdot e.\mathrm{permCongr}(q). $$$$

Lean4

@[simp]
theorem _root_.Equiv.permCongr_mul (e : α ≃ β) (p q : Perm α) : e.permCongr (p * q) = e.permCongr p * e.permCongr q :=
  permCongr_trans e q p |>.symm

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