permCongrHom_coe_equiv

Mathlib.Algebra.Group.End

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

English

The underlying equivalence of the conjugation homomorphism e.permCongrHom is e.permCongr.

Русский

Базовая эквивалентность сопряжения e.permCongrHom равна e.permCongr.

LaTeX

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

Lean4

@[simp]
theorem _root_.Equiv.permCongrHom_coe_equiv (e : α ≃ β) : (↑e.permCongrHom : Perm α ≃ Perm β) = e.permCongr :=
  rfl

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

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

Разделы

Аффилиация

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