Commit 2025-08-03 07:56 3d31f1f2

View on Github →

chore: replace norm_num with simp where applicable (#24064) Consider replacing a tactic with a (ahem) simpler alternative. Fairly neutral performance implications, just depends on whether we would like to encourage people to use simp where applicable.

Estimated changes

modified theorem Imo2006Q3.four_pow_four_pos
modified theorem Imo2006Q3.zero_lt_32
modified theorem Complex.two_pi_I_ne_zero
modified theorem Complex.I_pow_four