mathlib

f7953c0e - feat(algebra/big_operators/norm_num): add limited support for finset intervals (#16518)