conjugateEquiv_symm_comm — Mathlib

English

The symmetric version of the iterated mate-conjugate equality holds: (mateEquiv adj1 adj2).symm ((mateEquiv adj4 adj3).symm α) = (conjugateEquiv (adj1.adj4) (adj3.adj2)).symm α.

Русский

Симметричное утверждение к предыдущему: …

LaTeX

$$$$ (\\operatorname{mateEquiv} adj_1 adj_2)\\!^{\\,-1}((\\operatorname{mateEquiv} adj_4 adj_3)^{\\,-1} \\alpha) = (\\operatorname{conjugateEquiv} (adj_1 \\cdot adj_4) (adj_3 \\cdot adj_2))^{\\,-1} \\alpha. $$$$

Lean4

theorem conjugateEquiv_symm_comm {α : r₁ ⟶ r₂} {β : r₂ ⟶ r₁} (αβ : α ≫ β = 𝟙 _) :
    (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 _ := by
  rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

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