79542904

Date: 2025-03-29 07:30:58
Score: 0.5
Natty:
Report link

In lean4, you use:

import Mathlib.Algebra.BigOperators.Basic

open Finset BigOperators

/- rest of code -/
Reasons:
  • Low length (1):
  • Has code block (-0.5):
Posted by: Luiz Martins