Theorem Complex.I_zpow_bit1

Modification history

2024-05-18 16:15
Mathlib/Data/Complex/Basic.lean
chore: Delete `Algebra.GroupPower.Basic`, `Algebra.GroupWithZero.Bitwise` (#11855) …
Deleted Complex.I_zpow_bit1View on Github →
2023-11-10 08:35
Mathlib/Data/Complex/Basic.lean
chore(Data/Complex/Basic): add missing cast lemmas for `Rat` (#8225) …
Modified Complex.I_zpow_bit1View on Github →
2023-03-13 12:48
Mathlib/Data/Complex/Basic.lean
chore: tidy Data/Complex/Basic (#2844)
Added Complex.I_zpow_bit1View on Github →