Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2023-01-19 15:23
9292ecc2
View on Github →
feat(analysis/special_functions/pow): interaction between
cpow
and
inv
/
conj
(
#18137
)
Estimated changes
Modified
src/analysis/special_functions/pow.lean
added
theorem
complex.conj_cpow
added
theorem
complex.conj_cpow_eq_ite
added
theorem
complex.cpow_conj
added
theorem
complex.inv_cpow
added
theorem
complex.inv_cpow_eq_ite'
added
theorem
complex.inv_cpow_eq_ite