mkPiAlgebraFin_apply

Mathlib.LinearAlgebra.Multilinear.Basic

URI: https://scilib.ai/kg/mathlib#MultilinearMap.mkPiAlgebraFin_apply

English

The value of mkPiAlgebraFin on a constant function a is a^n, where n = length of index set.

Русский

Значение mkPiAlgebraFin на константное отображение a равно a^n, где n — длина множества индексов.

LaTeX

$$$$\mathrm{mkPiAlgebraFin}_R^{n,A}(\,a\,) = a^n.$$$$

Lean4

@[simp]
theorem mkPiAlgebraFin_apply (m : Fin n → A) : MultilinearMap.mkPiAlgebraFin R n A m = (List.ofFn m).prod :=
  rfl

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

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

Разделы

Аффилиация

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