coe_smulℝ

Mathlib.NumberTheory.ModularForms.SlashInvariantForms

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

English

For a slash-invariant form f and a real-scalar n, (n • f) is the function sending z to n f(z).

Русский

Для формЫ f и вещественного скаляра n: (n • f)(z) = n f(z).

LaTeX

$$$$ (n \\cdot f)(z) = n \\cdot f(z). $$$$

Lean4

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

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

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

Разделы

Аффилиация

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