∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k_1 k_2 : ℤ} (f : ModularForm Γ k_1) (g : ModularForm Γ k_2),
  MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ)
    (⇑f.toSlashInvariantForm * ⇑g.toSlashInvariantForm)