English
If M and M₂ are linearly isomorphic, then the endomorphism rings End_R(M) and End_R(M₂) are isomorphic via conjugation.
Русский
Если пространства M и M₂ линейно изоморфны, то кольца эндоморфизмов End_R(M) и End_R(M₂) изоморфны через сопряжение.
LaTeX
$$$\text{conj} : End_{R_1}(M_1) \simeq End_{R_2}(M_2)$ given an isomorphism e: M_1 \simeq M_2$$$
Lean4
/-- If `M` and `M₂` are linearly isomorphic then the two spaces of linear maps from `M` and `M₂` to
themselves are linearly isomorphic.
See `LinearEquiv.conjRingEquiv` for the isomorphism between endomorphism rings,
which works over a not necessarily commutative semiring. -/
-- TODO: upgrade to AlgEquiv (but this file currently cannot import AlgEquiv)
def conj (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') : Module.End R₁' M₁' ≃ₛₗ[σ₁'₂'] Module.End R₂' M₂' :=
arrowCongr e e
