mul_slash_SL2 — Mathlib

English

For k1, k2 ∈ ℤ, A ∈ SL(2,ℤ), and f, g: ℍ → ℂ, we have (f * g) ∣[k1+k2] A = (f ∣[k1] A) * (g ∣[k2] A).

Русский

Для k1,k2 ∈ ℤ, A ∈ SL(2,ℤ) и функций f,g: ℍ → ℂ выполняется (f g) ∣[k1+k2] A = (f ∣[k1] A) (g ∣[k2] A).

LaTeX

$$$ (f g) \lvert[k_1+k_2] A = (f \lvert[k_1] A) (g \lvert[k_2] A) $$$

Lean4

theorem mul_slash_SL2 (k1 k2 : ℤ) (A : SL(2, ℤ)) (f g : ℍ → ℂ) : (f * g) ∣[k1 + k2] A = f ∣[k1] A * g ∣[k2] A := by
  simp [SL_slash, mul_slash]

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