English
The canonical coercion from the restricted-scalar map back to the original map is the identity on the underlying functions.
Русский
Каноническое преобразование из отображения с ограничением скаляров обратно к исходному отображению не меняет функциональный смысл.
LaTeX
$$$ coe_{restrictScalars} = \\mathrm{id} $ on functions$$
Lean4
/-- Transfer the arguments to a map along an equivalence between argument indices.
The naming is derived from `Finsupp.domCongr`, noting that here the permutation applies to the
domain of the domain. -/
@[simps apply]
def domDomCongr (σ : ι₁ ≃ ι₂) (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) : MultilinearMap R (fun _ : ι₂ => M₂) M₃
where
toFun v := m fun i => v (σ i)
map_update_add' v i a
b := by
letI := σ.injective.decidableEq
simp_rw [Function.update_apply_equiv_apply v]
rw [m.map_update_add]
map_update_smul' v i a
b := by
letI := σ.injective.decidableEq
simp_rw [Function.update_apply_equiv_apply v]
rw [m.map_update_smul]
