iterated_mateEquiv_conjugateEquiv_symm

English

If α is a mate in a square, then iterating the conjugation on the right yields the same result as taking the symm of the iterated conjugation.

Русский

Если α является мейтом в квадрате, повторное применение сопряжения справа даёт тот же результат, что и симм итерации сопряжения.

LaTeX

$$$$ (\\text{iterated conjugation})^{-1}(α) = (\\text{iterated conj})^{-1}(α). $$$$

Lean4

theorem iterated_mateEquiv_conjugateEquiv_symm (α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁) :
    (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) =
      (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm α :=
  by
  rw [Equiv.eq_symm_apply, ← iterated_mateEquiv_conjugateEquiv]
  simp only [Equiv.apply_symm_apply]

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