smul_iff — Mathlib

English

Zero at cusp is preserved under scaling by GL(2,R) translations in the cusp action.

Русский

Нуль в cusp сохраняется при масштабировании действием GL(2,R) в cusp-операции.

LaTeX

$$IsZeroAt(g·c,f,k) ↔ IsZeroAt(c,f|[k]g,k)$$

Lean4

theorem smul_iff : IsZeroAt (g • c) f k ↔ IsZeroAt c (f ∣[k] g) k :=
  by
  rw [IsZeroAt, IsZeroAt, (Equiv.mulLeft g⁻¹).forall_congr_left]
  simp [MulAction.mul_smul, ← SlashAction.slash_mul]

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