permCongr_def

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.permCongr_def

English

For e : α' ≃ β' and p : Equiv.Perm α', e.permCongr p = (e.symm.trans p).trans e. The induced permutation on β' is the conjugate of p by e.

Русский

Для e : α' ≃ β' и p : Perm α' имеем e.permCongr p = (e^{-1} p e). Конъюгация перестановок по e.

LaTeX

$$$e.p\mathrm{ermCongr}(p) = (e^{-1}\,.trans\,p).trans\,e$$$

Lean4

theorem permCongr_def (p : Equiv.Perm α') : e.permCongr p = (e.symm.trans p).trans e :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru