Commit 2023-03-13 12:48 3f8368b6

View on Github →

chore: tidy Data/Complex/Basic (#2844)

Estimated changes

added theorem Complex.I_im
added theorem Complex.I_mul
added theorem Complex.I_mul_I
added theorem Complex.I_mul_im
added theorem Complex.I_mul_re
added theorem Complex.I_ne_zero
added theorem Complex.I_pow_bit0
added theorem Complex.I_pow_bit1
added theorem Complex.I_re
added theorem Complex.I_sq
added theorem Complex.I_zpow_bit0
added theorem Complex.I_zpow_bit1
deleted theorem Complex.i_im
deleted theorem Complex.i_mul
deleted theorem Complex.i_mul_I
deleted theorem Complex.i_mul_im
deleted theorem Complex.i_mul_re
deleted theorem Complex.i_ne_zero
deleted theorem Complex.i_pow_bit0
deleted theorem Complex.i_pow_bit1
deleted theorem Complex.i_re
deleted theorem Complex.i_sq
deleted theorem Complex.i_zpow_bit0
deleted theorem Complex.i_zpow_bit1
added theorem Complex.ofReal_ofNat