coe_smul

Mathlib.NumberTheory.ModularForms.SlashInvariantForms

URI: https://scilib.ai/kg/mathlib#SlashInvariantForm.coe_smul

English

The scalar action commutes with the underlying function: (n • f) = n • f as functions, for any scalar n in α.

Русский

Скалярное действие совместимо с приведением к функциям: (n • f) = n • f как функции.

LaTeX

$$$$ (n \\cdot f)(z) = n \\cdot f(z) \\quad (z \\in \\mathbb{H}). $$$$

Lean4

@[simp]
theorem coe_smul (f : SlashInvariantForm Γ k) (n : α) : ⇑(n • f) = n • ⇑f :=
  rfl

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

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

Разделы

Аффилиация

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