English
Let e be a linear isomorphism between two finite-rank free R-modules M1 and M2, and φ a linear endomorphism of M1. Conjugating φ by e yields a new endomorphism e.conj φ on M2. The characteristic polynomial is invariant under this similarity transformation: χ_{e.conj φ} = χ_{φ}.
Русский
Пусть e — линейное взаимодополнение между M1 и M2, а φ — линейное преобразование на M1. Приведение φ к эквивалентной форме на M2 через сопряжение сохраняет характеристический многочлен: χ_{e.conj φ} = χ_{φ}.
LaTeX
$$$\operatorname{charpoly}(e \cdot \phi \cdot e^{-1}) = \operatorname{charpoly}(\phi)$$$
Lean4
@[simp]
theorem charpoly_conj (e : M₁ ≃ₗ[R] M₂) (φ : Module.End R M₁) : (e.conj φ).charpoly = φ.charpoly :=
by
let b := chooseBasis R M₁
rw [← LinearMap.charpoly_toMatrix φ b, ← LinearMap.charpoly_toMatrix (e.conj φ) (b.map e)]
congr 1
ext i j : 1
simp [LinearMap.toMatrix, LinearEquiv.conj_apply]
