Commit 2023-05-18 09:26 f035a653

View on Github →

feat: port Analysis.SpecialFunctions.Pow.Complex (#4070)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean

added theorem Complex.conj_cpow

added theorem Complex.conj_cpow_eq_ite

added theorem Complex.cpow_add

added theorem Complex.cpow_conj

added theorem Complex.cpow_def

added theorem Complex.cpow_def_of_ne_zero

added theorem Complex.cpow_eq_pow

added theorem Complex.cpow_eq_zero_iff

added theorem Complex.cpow_int_cast

added theorem Complex.cpow_mul

added theorem Complex.cpow_nat_cast

added theorem Complex.cpow_nat_inv_pow

added theorem Complex.cpow_neg

added theorem Complex.cpow_neg_one

added theorem Complex.cpow_one

added theorem Complex.cpow_sub

added theorem Complex.cpow_two

added theorem Complex.cpow_zero

added theorem Complex.eq_zero_cpow_iff

added theorem Complex.inv_cpow

added theorem Complex.inv_cpow_eq_ite'

added theorem Complex.inv_cpow_eq_ite

added theorem Complex.mul_cpow_of_real_nonneg

added theorem Complex.one_cpow

added theorem Complex.zero_cpow

added theorem Complex.zero_cpow_eq_iff