Commit 2023-10-30 12:55 fd0d3acc

View on Github →

feat: explicit formula for the complex square root (#7968) Also add formula for cos (x / 2), sin (x / 2) and golf some proofs.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

added theorem Complex.abs_mul_cos_arg

added theorem Complex.abs_mul_sin_arg

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

added theorem Complex.abs_cpow_inv_two_im

added theorem Complex.cpow_inv_two_im_eq_neg_sqrt

added theorem Complex.cpow_inv_two_im_eq_sqrt

added theorem Complex.cpow_inv_two_re

added theorem Complex.cpow_ofReal

added theorem Complex.cpow_ofReal_im

added theorem Complex.cpow_ofReal_re

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

added theorem Real.abs_sin_half

added theorem Real.cos_half

added theorem Real.sin_half_eq_neg_sqrt

added theorem Real.sin_half_eq_sqrt

Modified Mathlib/Data/Complex/Exponential.lean

added theorem Real.sin_sq_eq_half_sub