conj_symm_conj — Mathlib

English

Let e be a linear equivalence between two modules M1' and M2' and let f be a linear endomorphism on M1'. Then transporting f to M2' via e and then transporting back yields the original endomorphism: e.symm.conj (e.conj f) = f.

Русский

Пусть e — линейное эквивалентное отображение между модулями M1' и M2', а f — линейный эндоморфизм на M1'. Тогда перенос f на M2' по e и последующий обратный перенос возвращают исходный эндоморфизм: e.symm.conj (e.conj f) = f.

LaTeX

$$$ e^{-1} \circ (e \circ f \circ e^{-1}) \circ e = f $$$

Lean4

@[simp]
theorem conj_symm_conj (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁') : e.symm.conj (e.conj f) = f := by ext;
  simp [conj_apply]

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