Trace H fixed of smul

theorem traceH_fixed_of_smul (α k g : ℕ) (hg : Odd g)    (himg : (Hexp α k).image (fun i => (g * i) % 2 ^ (α + 1)) = Hexp α k)    (a : Rq (powTwoCyclotomic (R := R) α)) :    galoisRingHom α g hg (traceH α k a) = traceH α k a := by  have hodd := Hexp_odd_mem α k  have hinj : Set.InjOn (fun i => (g * i) % 2 ^ (α + 1)) (Hexp α k) :=    Finset.injOn_of_card_image_eq (by rw [himg])  unfold traceH traceOver  rw [map_sum,    Finset.sum_congr rfl fun i hi => by      rw [galoisRingHom_apply, galoisAut_comp α g i hg (hodd i hi), galoisAut_periodic]]  conv_rhs => rw [← himg]  rw [Finset.sum_image fun x hx y hy h => hinj hx hy h]