Theorem Complex.I_zpow_eq_zpow_mod

Modification history

2026-07-24 11:04
Mathlib/Data/Complex/Basic.lean
feat(Data/Complex/Basic): add simproc to reduce powers of I (#39506) …
Added Complex.I_zpow_eq_zpow_modView on Github →