Theorem Complex.I_pow_bit1

Modification history

2024-07-15 23:26
Mathlib/Data/Complex/Basic.lean
chore: remove lemmas about bit0/bit1 (#14765) …
Deleted Complex.I_pow_bit1View on Github →
2024-07-15 11:16
Mathlib/Data/Complex/Basic.lean
chore: remove bit0/bit1 and associated lemmas (#14745) …
Modified Complex.I_pow_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_pow_bit1View on Github →
2023-03-13 12:48
Mathlib/Data/Complex/Basic.lean
chore: tidy Data/Complex/Basic (#2844)
Added Complex.I_pow_bit1View on Github →