permCongrHom_coe

Mathlib.Algebra.Group.End

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

English

The function part of e.permCongrHom agrees with the function e.permCongr: the coe of the hom equals the conjugation by e.

Русский

Элемент-образующая e.permCongrHom совпадает с конъюгацией e: Perm α → Perm β.

LaTeX

$$$$ \bigl( \uparrow e.\mathrm{permCongrHom} \bigr) = e.\mathrm{permCongr}. $$$$

Lean4

@[simp]
theorem _root_.Equiv.permCongrHom_coe (e : α ≃ β) : ⇑e.permCongrHom = ⇑e.permCongr :=
  rfl

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

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

Разделы

Аффилиация

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