∀ {G M : Type} [inst : Group G] [inst_1 : Fintype G] [inst_2 : CommGroup M] [inst_3 : MulDistribMulAction G M]
  (x : Additive M), Additive.toMul ((Representation.ofMulDistribMulAction G M).norm x) = ∏ g, g • Additive.toMul x