Commit 2023-11-03 06:27 9eab0567

View on Github →

feat(SpecialFunctions/Pow): prove cpow_int_mul etc (#7942)

  • Add Complex.cpow_int_mul, Complex.cpow_mul_int, Complex.cpow_nat_mul, and Complex.cpow_mul_nat.
  • Generalize Complex.cpow_two to Complex.cpow_ofNat.
  • Golf some proofs using new lemmas. Motivated by a lemma in the Mandelbrot set connectedness project. Co-Authored-By: @girving

Estimated changes

modified theorem Complex.cpow_int_cast
added theorem Complex.cpow_int_mul'
added theorem Complex.cpow_int_mul
added theorem Complex.cpow_mul_int
added theorem Complex.cpow_mul_nat
added theorem Complex.cpow_mul_ofNat
modified theorem Complex.cpow_nat_cast
added theorem Complex.cpow_nat_mul'
added theorem Complex.cpow_nat_mul
added theorem Complex.cpow_ofNat
added theorem Complex.cpow_ofNat_mul
modified theorem Complex.cpow_two