Commit 2026-07-24 11:04 587ae263

feat(Data/Complex/Basic): add simproc to reduce powers of I (#39506) This is enabled by default to make eg i^5 simplify automatically. We intentionally require the exponent to be a numeral, as this is intended to be a reduction statement, and for symbolic n, the lemma I_pow_eq_pow_mod should be used instead. Note that we can't have I_pow_eq_pow_mod as a simp lemma due to looping.