fourierSMulRight_apply — Mathlib

English

The right-hand side construction maps a function f : V → E to a family of linear functionals on W, given by a scalar multiple of the L v w-action applied to f(v). In particular, for each v ∈ V, w ∈ W, the value is - (2π i) L(v,w) · f(v).

Русский

Для каждой пары v ∈ V, w ∈ W значение равно - (2π i) L(v,w) · f(v).

LaTeX

$$$(\\text{fourierSMulRight } L f v)(w) = -(2\\pi i) \\; L(v,w) \\; f(v)$$$

Lean4

@[simp]
theorem fourierSMulRight_apply (v : V) (w : W) : fourierSMulRight L f v w = -(2 * π * I) • L v w • f v :=
  rfl

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