`gTerm` is homogeneous of degree `-3`

import Definitions.Def_BlockCycleRotation_Remark21
import Mathlib

open BlockCycleRotation
open Real Finset Filter Topology

theorem BlockCycleRotation.gTerm_smul {k a a' : ℕ} (hk : 0 < k) (h1 : 1 ≤ a') (h2 : a' < a) :
    gTerm (k * a, k * a') = gTerm (a, a') / (k : ℝ) ^ 3 := by sorry