English
Given a family e_i of linear equivalences e_i: β1_i ≃ₗ β2_i, there is a canonical linear equivalence between the dependent finite-support functions: (Π₀ i, β1_i) ≃ₗ (Π₀ i, β2_i).
Русский
Дана семья линейных эквалентностей e_i: β1_i ≃ₗ β2_i. Существует каноническое линейное эквалентное отображение между зависимыми функциями с конечной поддержкой: (Π₀ i, β1_i) ≃ₗ (Π₀ i, β2_i).
LaTeX
$$$\\mathrm{mapRange.linearEquiv}\\; e : (Π₀ i, β1 i) \\simeq_ℓ (Π₀ i, β2 i)$$$
Lean4
/-- `DFinsupp.mapRange.linearMap` as a `LinearEquiv`. -/
@[simps apply]
def linearEquiv (e : ∀ i, β₁ i ≃ₗ[R] β₂ i) : (Π₀ i, β₁ i) ≃ₗ[R] Π₀ i, β₂ i :=
{ mapRange.addEquiv fun i => (e i).toAddEquiv,
mapRange.linearMap fun i =>
(e i).toLinearMap with
toFun := mapRange (fun i x => e i x) fun i => (e i).map_zero
invFun := mapRange (fun i x => (e i).symm x) fun i => (e i).symm.map_zero }
