permCongrHom_trans — Mathlib

English

Conjugation respects composition: permCongrHom(e) ∘ permCongrHom(e') = permCongrHom(e ∘ e').

Русский

Сопряжение сохраняет композицию: permCongrHom(e) ∘ permCongrHom(e') = permCongrHom(e ∘ e').

LaTeX

$$$$ \mathrm{permCongrHom}(e) \circ \mathrm{permCongrHom}(e') = \mathrm{permCongrHom}(e \circ e'). $$$$

Lean4

@[simp]
theorem _root_.Equiv.permCongrHom_trans (e : α ≃ β) (e' : β ≃ γ) :
    e.permCongrHom.trans e'.permCongrHom = (e.trans e').permCongrHom :=
  rfl

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