English
DFinsupp.equivCongrLeft acts as a linear equivalence reflecting index permutation on a product of indices.
Русский
DFinsupp.equivCongrLeft действует как линейное эквивалентное отображение, отражающее перестановку индексов над произведением индексов.
LaTeX
$$$\\mathrm{domLCongr}(e) : (\\Pi_0 i, M_i) \\simeq_ℓ (\\Pi_0 i, M_{e^{-1}(i)})$$$
Lean4
/-- `DFinsupp.mapRange` as a `LinearMap`. -/
@[simps! apply]
def linearMap (f : ∀ i, β₁ i →ₗ[R] β₂ i) : (Π₀ i, β₁ i) →ₗ[R] Π₀ i, β₂ i :=
{
mapRange.addMonoidHom fun i =>
(f i).toAddMonoidHom with
toFun := mapRange (fun i x => f i x) fun i => (f i).map_zero
map_smul' := fun r => mapRange_smul _ (fun i => (f i).map_zero) _ fun i => (f i).map_smul r }
