no goals
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
⊢ multiplicativeEnergy s univ = Fintype.card α * card s ^ 2
rw [multiplicativeEnergy_comm, multiplicativeEnergy_univ_left]