Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finpartition.coe_energy

Modification history

2023-05-19 22:52
src/combinatorics/simple_graph/regularity/energy.lean
feat(combinatorics/simple_graph/regularity): Increment partition (#19051) …
Added finpartition.coe_energyView on Github →