SL_smul_slash — Mathlib

English

For any α with reasonable SMul structure on ℂ, we have (c • f) ∣[k] A = c • (f ∣[k] A) for SL(2,ℤ) actions.

Русский

При наличии подходящей операции умножения на скаляры на ℂ выполняется (c • f) ∣[k] A = c • (f ∣[k] A) для SL2Z-действия.

LaTeX

$$$ (c \cdot f) \lvert[k] A = c \cdot (f \lvert[k] A) $$$

Lean4

@[simp]
theorem SL_smul_slash {α : Type*} [SMul α ℂ] [IsScalarTower α ℂ ℂ] (k : ℤ) (A : SL(2, ℤ)) (f : ℍ → ℂ) (c : α) :
    (c • f) ∣[k] A = c • f ∣[k] A := by
  ext τ : 1
  simp [SL_slash_apply, Pi.smul_apply, smul_mul_assoc]

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