coe_translate

Mathlib.NumberTheory.ModularForms.SlashInvariantForms

URI: https://scilib.ai/kg/mathlib#SlashInvariantForm.coe_translate

English

The translated form equals the slash action of g on f: translate(f,g) = f ∣[k] g.

Русский

Перенесённая форма равна действию slash на f: translate(f,g) = f ∣[k] g.

LaTeX

$$$\text{translate}(f,g) = f ∣[k] g.$$$

Lean4

@[simp]
theorem coe_translate [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ℝ) : translate f g = ⇑f ∣[k] g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru