smul_applyℝ — Mathlib

English

The action by a real scalar on SlashInvariantForm Γ k is given by pointwise multiplication of the scalar with the function value.

Русский

Действие вещественного скаляра на SlashInvariantForm Γ k задаётся точечным умножением на значение функции.

LaTeX

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

Lean4

@[simp]
theorem smul_applyℝ (f : SlashInvariantForm Γ k) (n : α) (z : ℍ) : (n • f) z = n • f z :=
  rfl

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