English
Given an R-linear isomorphism e, there is a natural S-linear isomorphism between the spaces of linear maps M2 → M and M3 → M, obtained by precomposition with e.
Русский
Дан R-линейный изоморфизм e, существует естественный S-линейный изоморфизм между пространствами линейных отображений M2 → M и M3 → M, получаемый преддекомпозицией с e.
LaTeX
$$$ (M_2 \to_{\mathbb{R}} M) \simeq_{\mathsf{S}} (M_3 \to_{\mathbb{R}} M) $$$
Lean4
/-- Given an `R`-module `M` and an equivalence `m ≃ n` between arbitrary types,
construct a linear equivalence `(n → M) ≃ₗ[R] (m → M)` -/
def funCongrLeft (e : m ≃ n) : (n → M) ≃ₗ[R] m → M :=
LinearEquiv.ofLinear (funLeft R M e) (funLeft R M e.symm)
(LinearMap.ext fun x ↦ funext fun i ↦ by rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id])
(LinearMap.ext fun x ↦ funext fun i ↦ by rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id])
