conjugateEquiv_symm_id — Mathlib

English

The symmetrized conjugation sends the identity on the right side back to the identity on the left: (conjugateEquiv adj1 adj1).symm (id_{r1}) = id_{l1}.

Русский

Симметричное сопряжение отправляет тождественный морфизм справа в тождественный слева: (conjugateEquiv adj1 adj1).symm (id_{r1}) = id_{l1}.

LaTeX

$$$$ (conjugateEquiv adj_1 adj_1).symm (\\mathrm{id}_{r_1}) = \\mathrm{id}_{l_1}. $$$$

Lean4

@[simp]
theorem conjugateEquiv_symm_id : (conjugateEquiv adj₁ adj₁).symm (𝟙 _) = 𝟙 _ := by
  rw [Equiv.symm_apply_eq, conjugateEquiv_id]

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