smul_apply — Mathlib

English

The scalar action commutes with the underlying function: for any α-linear scalar n, (n • f)(z) = n • f(z).

Русский

Действие скаляра коммутирует с функцией: для любого скалярного множителя n, (n • f)(z) = n • f(z).

LaTeX

$$$\forall f: \mathrm{CuspForm}(\Gamma,k), \forall n, \; (n \cdot f) = n \cdot f$ as functions.$$

Lean4

@[simp]
theorem smul_apply (f : CuspForm Γ k) (n : α) {z : ℍ} : (n • f) z = n • f z :=
  rfl

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