permCongr_trans — Mathlib

English

Conjugation by e respects composition: (e.permCongr p) . (e.permCongr p') = e.permCongr (p . p').

Русский

Конъюгация по e сохраняет композицию перестановок: conj_e(p) ∘ conj_e(p') = conj_e(p ∘ p').

LaTeX

$$$(e\text{.permCongr } p)\,\text{.trans }(e\text{.permCongr } p') = e\text{.permCongr } (p\circ p')$$

Lean4

theorem permCongr_trans (p p' : Equiv.Perm α') : (e.permCongr p).trans (e.permCongr p') = e.permCongr (p.trans p') := by
  grind

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