complexBasis_apply

Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

URI: https://scilib.ai/kg/mathlib#AddChar.complexBasis_apply

English

For any ψ in AddChar α ℂ, the complexBasis evaluated at ψ equals ψ.

Русский

Для любого ψ ∈ AddChar α ℂ комплексная база применяется так, что её значение равно ψ.

LaTeX

$$$ complexBasis(α)\; ψ = ψ $$$

Lean4

@[simp]
theorem complexBasis_apply (ψ : AddChar α ℂ) : complexBasis α ψ = ψ := by rw [coe_complexBasis]

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

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

Разделы

Аффилиация

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