smul_slash — Mathlib

English

For any f, g, c with c a scalar, we have (c • f) ∣[k] A = c • (f ∣[k] A).

Русский

При любом f, g и скаляре c выполняется: (c • f) ∣[k] A = c • (f ∣[k] A).

LaTeX

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

Lean4

theorem smul_slash (k : ℤ) (A : GL (Fin 2) ℝ) (f : ℍ → ℂ) (c : ℂ) : (c • f) ∣[k] A = σ A c • f ∣[k] A :=
  by
  ext τ : 1
  simp only [slash_apply, Pi.smul_apply, smul_eq_mul, map_mul, mul_assoc]

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