Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-11-23 09:38
8f681f12
View on Github →
chore(data/complex): add a few simp lemmas (
#10395
)
Estimated changes
Modified
src/data/complex/basic.lean
added
theorem
complex.abs_pow
added
theorem
complex.abs_zpow
Modified
src/data/complex/exponential.lean
modified
theorem
complex.abs_cos_add_sin_mul_I
added
theorem
complex.abs_exp_of_real_mul_I