permCongrHom_symm — Mathlib

English

The inverse of the conjugation homomorphism corresponds to conjugation by the inverse equivalence: (permCongrHom(e))^{-1} = permCongrHom(e^{-1}).

Русский

Обратный гомоморфизм сопряжения соответствует сопряжению перестановки обратной эквивалентностью: (permCongrHom(e))^{-1} = permCongrHom(e^{-1}).

LaTeX

$$$$ \mathrm{permCongrHom\_symm}(e): \bigl(\mathrm{permCongrHom}(e)\bigr)^{-1} = \mathrm{permCongrHom}(e^{-1}). $$$$

Lean4

@[simp]
theorem _root_.Equiv.permCongrHom_symm (e : α ≃ β) : e.permCongrHom.symm = e.symm.permCongrHom :=
  rfl

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