Commit 2023-11-10 08:35 a2441385

View on Github →

chore(Data/Complex/Basic): add missing cast lemmas for Rat (#8225) One Nat lemma was duplicated

Estimated changes

modified theorem Complex.I_pow_bit0
modified theorem Complex.I_pow_bit1
modified theorem Complex.I_zpow_bit0
modified theorem Complex.I_zpow_bit1
deleted theorem Complex.abs_cast_nat
modified theorem Complex.int_cast_im
modified theorem Complex.int_cast_re
modified theorem Complex.nat_cast_im
modified theorem Complex.nat_cast_re
modified theorem Complex.ofReal_int_cast
modified theorem Complex.ofReal_nat_cast
modified theorem Complex.ofReal_rat_cast
modified theorem Complex.rat_cast_im
modified theorem Complex.rat_cast_re