coe_multilinearMap

Mathlib.LinearAlgebra.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#AlternatingMap.coe_multilinearMap

English

The evaluation of f as a multilinear map agrees with its evaluation as a function.

Русский

Оценка f как много-линейного отображения совпадает с её оценкой как функции.

LaTeX

$$Eq (MultilinearMap.instFunLikeForall.coe f.toMultilinearMap) (AlternatingMap.instFunLike.coe f)$$

Lean4

@[simp, norm_cast]
theorem coe_multilinearMap : ⇑(f : MultilinearMap R (fun _ : ι => M) N) = f :=
  rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru