symm_self_conj — Mathlib

English

Conjugating by α.symm after α.conj returns the original endomorphism: α.symm.conj (α.conj f) = f.

Русский

Сочетание конъюгации через симметричный изоморфизм обратно возвращает исходное: α.symm.conj (α.conj f) = f.

LaTeX

$$$\\alpha.\\mathrm{symm}.\\mathrm{conj}(\\alpha.\\mathrm{conj} f) = f$$$

Lean4

@[simp]
theorem symm_self_conj (f : End X) : α.symm.conj (α.conj f) = f := by rw [← trans_conj, α.self_symm_id, refl_conj]

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