α : Type u_2
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
⊢ ↑((∑ uv in offDiag P.parts, SimpleGraph.edgeDensity G uv.fst uv.snd ^ 2) / ↑(card P.parts ^ 2)) =
    ↑(∑ uv in offDiag P.parts, SimpleGraph.edgeDensity G uv.fst uv.snd ^ 2) / ↑(↑(card P.parts) ^ 2)
α : Type u_2
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
⊢ ↑(energy P G) = ↑(∑ uv in offDiag P.parts, SimpleGraph.edgeDensity G uv.fst uv.snd ^ 2) / ↑(↑(card P.parts) ^ 2)
rw [energy]
no goals
α : Type u_2
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
⊢ ↑((∑ uv in offDiag P.parts, SimpleGraph.edgeDensity G uv.fst uv.snd ^ 2) / ↑(card P.parts ^ 2)) =
    ↑(∑ uv in offDiag P.parts, SimpleGraph.edgeDensity G uv.fst uv.snd ^ 2) / ↑(↑(card P.parts) ^ 2)
norm_cast