mathlib

6054f7c9 - chore(number_theory/sum_four_squares): slightly shorten proof (#2457)