Commit 2023-10-30 12:55 d1f2a8e2

View on Github →

feat(Data/Complex): add lemmas like div_ofReal_re (#8024)

Estimated changes

Modified Mathlib/Data/Complex/Basic.lean

added theorem Complex.div_int_cast

added theorem Complex.div_int_cast_im

added theorem Complex.div_int_cast_re

added theorem Complex.div_nat_cast

added theorem Complex.div_nat_cast_im

added theorem Complex.div_nat_cast_re

added theorem Complex.div_ofNat

added theorem Complex.div_ofNat_im

added theorem Complex.div_ofNat_re

added theorem Complex.div_ofReal

added theorem Complex.div_ofReal_im

added theorem Complex.div_ofReal_re

added theorem Complex.div_rat_cast

added theorem Complex.div_rat_cast_im

added theorem Complex.div_rat_cast_re