Commit 2023-02-18 08:47 297619ec

View on Github →

chore(number_theory/sum_four_squares): squeeze simps (#18461) This proof goes from 20s to 8s. Adding a missing norm_cast lemma makes it possible to replace some simps with push_cast

Estimated changes

Modified src/data/zmod/basic.lean

modified theorem zmod.coe_val_min_abs

Modified src/number_theory/sum_four_squares.lean