English
There is a canonical linear equivalence between finitely supported M-valued functions on ι and finitely supported N-valued functions on κ, obtained from a domain equivalence ι ≃ κ and a codomain linear equivalence M ≃ₛₗ[σ] N.
Русский
Существует каноническое линейное эквивалентное отображение между функциями с конечной опорой от ι в M и функциями с конечной опорой от κ в N, получаемое из эквивалентности домена ι ≃ κ и линейной эквалентности кодом M ≃ₛₗ[σ] N.
LaTeX
$$$lcongr\;{ι}\;{κ}\; (e_1 : ι \simeq κ)\; (e_2 : M \simeq_σₗ N) : (ι \to_0 M) \simeq_σ (κ \to_0 N)$$$
Lean4
/-- An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the
corresponding finitely supported functions. -/
def lcongr {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) : (ι →₀ M) ≃ₛₗ[σ] κ →₀ N :=
(Finsupp.domLCongr e₁).trans (mapRange.linearEquiv e₂)
