Documentation

Mathlib.Data.Complex.Trigonometric

Trigonometric and hyperbolic trigonometric functions #

This file contains the definitions of the sine, cosine, tangent, hyperbolic sine, hyperbolic cosine, and hyperbolic tangent functions.

def Complex.sin (z : ) :

The complex sine function, defined via exp

Equations
    Instances For
      def Complex.cos (z : ) :

      The complex cosine function, defined via exp

      Equations
        Instances For
          def Complex.tan (z : ) :

          The complex tangent function, defined as sin z / cos z

          Equations
            Instances For
              def Complex.cot (z : ) :

              The complex cotangent function, defined as cos z / sin z

              Equations
                Instances For
                  def Complex.sinh (z : ) :

                  The complex hyperbolic sine function, defined via exp

                  Equations
                    Instances For
                      def Complex.cosh (z : ) :

                      The complex hyperbolic cosine function, defined via exp

                      Equations
                        Instances For
                          def Complex.tanh (z : ) :

                          The complex hyperbolic tangent function, defined as sinh z / cosh z

                          Equations
                            Instances For
                              def Real.sin (x : ) :

                              The real sine function, defined as the real part of the complex sine

                              Equations
                                Instances For
                                  def Real.cos (x : ) :

                                  The real cosine function, defined as the real part of the complex cosine

                                  Equations
                                    Instances For
                                      def Real.tan (x : ) :

                                      The real tangent function, defined as the real part of the complex tangent

                                      Equations
                                        Instances For
                                          def Real.cot (x : ) :

                                          The real cotangent function, defined as the real part of the complex cotangent

                                          Equations
                                            Instances For
                                              def Real.sinh (x : ) :

                                              The real hypebolic sine function, defined as the real part of the complex hyperbolic sine

                                              Equations
                                                Instances For
                                                  def Real.cosh (x : ) :

                                                  The real hypebolic cosine function, defined as the real part of the complex hyperbolic cosine

                                                  Equations
                                                    Instances For
                                                      def Real.tanh (x : ) :

                                                      The real hypebolic tangent function, defined as the real part of the complex hyperbolic tangent

                                                      Equations
                                                        Instances For
                                                          theorem Complex.two_sinh (x : ) :
                                                          2 * sinh x = exp x - exp (-x)
                                                          theorem Complex.two_cosh (x : ) :
                                                          2 * cosh x = exp x + exp (-x)
                                                          @[simp]
                                                          theorem Complex.sinh_zero :
                                                          sinh 0 = 0
                                                          @[simp]
                                                          theorem Complex.sinh_neg (x : ) :
                                                          sinh (-x) = -sinh x
                                                          theorem Complex.sinh_add (x y : ) :
                                                          sinh (x + y) = sinh x * cosh y + cosh x * sinh y
                                                          @[simp]
                                                          theorem Complex.cosh_zero :
                                                          cosh 0 = 1
                                                          @[simp]
                                                          theorem Complex.cosh_neg (x : ) :
                                                          cosh (-x) = cosh x
                                                          theorem Complex.cosh_add (x y : ) :
                                                          cosh (x + y) = cosh x * cosh y + sinh x * sinh y
                                                          theorem Complex.sinh_sub (x y : ) :
                                                          sinh (x - y) = sinh x * cosh y - cosh x * sinh y
                                                          theorem Complex.cosh_sub (x y : ) :
                                                          cosh (x - y) = cosh x * cosh y - sinh x * sinh y
                                                          @[simp]
                                                          theorem Complex.ofReal_sinh_ofReal_re (x : ) :
                                                          (sinh x).re = sinh x
                                                          @[simp]
                                                          theorem Complex.ofReal_sinh (x : ) :
                                                          (Real.sinh x) = sinh x
                                                          @[simp]
                                                          theorem Complex.sinh_ofReal_im (x : ) :
                                                          (sinh x).im = 0
                                                          theorem Complex.ofReal_cosh_ofReal_re (x : ) :
                                                          (cosh x).re = cosh x
                                                          @[simp]
                                                          theorem Complex.ofReal_cosh (x : ) :
                                                          (Real.cosh x) = cosh x
                                                          @[simp]
                                                          theorem Complex.cosh_ofReal_im (x : ) :
                                                          (cosh x).im = 0
                                                          @[simp]
                                                          theorem Complex.cosh_ofReal_re (x : ) :
                                                          (cosh x).re = Real.cosh x
                                                          @[simp]
                                                          theorem Complex.tanh_zero :
                                                          tanh 0 = 0
                                                          @[simp]
                                                          theorem Complex.tanh_neg (x : ) :
                                                          tanh (-x) = -tanh x
                                                          @[simp]
                                                          theorem Complex.ofReal_tanh_ofReal_re (x : ) :
                                                          (tanh x).re = tanh x
                                                          @[simp]
                                                          theorem Complex.ofReal_tanh (x : ) :
                                                          (Real.tanh x) = tanh x
                                                          @[simp]
                                                          theorem Complex.tanh_ofReal_im (x : ) :
                                                          (tanh x).im = 0
                                                          @[simp]
                                                          theorem Complex.cosh_add_sinh (x : ) :
                                                          cosh x + sinh x = exp x
                                                          @[simp]
                                                          theorem Complex.sinh_add_cosh (x : ) :
                                                          sinh x + cosh x = exp x
                                                          @[simp]
                                                          theorem Complex.exp_sub_cosh (x : ) :
                                                          exp x - cosh x = sinh x
                                                          @[simp]
                                                          theorem Complex.exp_sub_sinh (x : ) :
                                                          exp x - sinh x = cosh x
                                                          @[simp]
                                                          theorem Complex.cosh_sub_sinh (x : ) :
                                                          cosh x - sinh x = exp (-x)
                                                          @[simp]
                                                          theorem Complex.sinh_sub_cosh (x : ) :
                                                          sinh x - cosh x = -exp (-x)
                                                          @[simp]
                                                          theorem Complex.cosh_sq_sub_sinh_sq (x : ) :
                                                          cosh x ^ 2 - sinh x ^ 2 = 1
                                                          theorem Complex.cosh_sq (x : ) :
                                                          cosh x ^ 2 = sinh x ^ 2 + 1
                                                          theorem Complex.sinh_sq (x : ) :
                                                          sinh x ^ 2 = cosh x ^ 2 - 1
                                                          theorem Complex.cosh_two_mul (x : ) :
                                                          cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2
                                                          theorem Complex.sinh_two_mul (x : ) :
                                                          sinh (2 * x) = 2 * sinh x * cosh x
                                                          theorem Complex.cosh_three_mul (x : ) :
                                                          cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
                                                          theorem Complex.sinh_three_mul (x : ) :
                                                          sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x
                                                          @[simp]
                                                          theorem Complex.sin_zero :
                                                          sin 0 = 0
                                                          @[simp]
                                                          theorem Complex.sin_neg (x : ) :
                                                          sin (-x) = -sin x
                                                          theorem Complex.two_sin (x : ) :
                                                          2 * sin x = (exp (-x * I) - exp (x * I)) * I
                                                          theorem Complex.two_cos (x : ) :
                                                          2 * cos x = exp (x * I) + exp (-x * I)
                                                          theorem Complex.sinh_mul_I (x : ) :
                                                          sinh (x * I) = sin x * I
                                                          theorem Complex.cosh_mul_I (x : ) :
                                                          cosh (x * I) = cos x
                                                          theorem Complex.tanh_mul_I (x : ) :
                                                          tanh (x * I) = tan x * I
                                                          theorem Complex.cos_mul_I (x : ) :
                                                          cos (x * I) = cosh x
                                                          theorem Complex.sin_mul_I (x : ) :
                                                          sin (x * I) = sinh x * I
                                                          theorem Complex.tan_mul_I (x : ) :
                                                          tan (x * I) = tanh x * I
                                                          theorem Complex.sin_add (x y : ) :
                                                          sin (x + y) = sin x * cos y + cos x * sin y
                                                          @[simp]
                                                          theorem Complex.cos_zero :
                                                          cos 0 = 1
                                                          @[simp]
                                                          theorem Complex.cos_neg (x : ) :
                                                          cos (-x) = cos x
                                                          theorem Complex.cos_add (x y : ) :
                                                          cos (x + y) = cos x * cos y - sin x * sin y
                                                          theorem Complex.sin_sub (x y : ) :
                                                          sin (x - y) = sin x * cos y - cos x * sin y
                                                          theorem Complex.cos_sub (x y : ) :
                                                          cos (x - y) = cos x * cos y + sin x * sin y
                                                          theorem Complex.sin_add_mul_I (x y : ) :
                                                          sin (x + y * I) = sin x * cosh y + cos x * sinh y * I
                                                          theorem Complex.sin_eq (z : ) :
                                                          sin z = sin z.re * cosh z.im + cos z.re * sinh z.im * I
                                                          theorem Complex.cos_add_mul_I (x y : ) :
                                                          cos (x + y * I) = cos x * cosh y - sin x * sinh y * I
                                                          theorem Complex.cos_eq (z : ) :
                                                          cos z = cos z.re * cosh z.im - sin z.re * sinh z.im * I
                                                          theorem Complex.sin_sub_sin (x y : ) :
                                                          sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
                                                          theorem Complex.cos_sub_cos (x y : ) :
                                                          cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
                                                          theorem Complex.sin_add_sin (x y : ) :
                                                          sin x + sin y = 2 * sin ((x + y) / 2) * cos ((x - y) / 2)
                                                          theorem Complex.cos_add_cos (x y : ) :
                                                          cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
                                                          @[simp]
                                                          theorem Complex.ofReal_sin_ofReal_re (x : ) :
                                                          (sin x).re = sin x
                                                          @[simp]
                                                          theorem Complex.ofReal_sin (x : ) :
                                                          (Real.sin x) = sin x
                                                          @[simp]
                                                          theorem Complex.sin_ofReal_im (x : ) :
                                                          (sin x).im = 0
                                                          @[simp]
                                                          theorem Complex.ofReal_cos_ofReal_re (x : ) :
                                                          (cos x).re = cos x
                                                          @[simp]
                                                          theorem Complex.ofReal_cos (x : ) :
                                                          (Real.cos x) = cos x
                                                          @[simp]
                                                          theorem Complex.cos_ofReal_im (x : ) :
                                                          (cos x).im = 0
                                                          @[simp]
                                                          theorem Complex.tan_zero :
                                                          tan 0 = 0
                                                          theorem Complex.tan_mul_cos {x : } (hx : cos x 0) :
                                                          tan x * cos x = sin x
                                                          @[simp]
                                                          theorem Complex.tan_neg (x : ) :
                                                          tan (-x) = -tan x
                                                          @[simp]
                                                          theorem Complex.ofReal_tan_ofReal_re (x : ) :
                                                          (tan x).re = tan x
                                                          @[simp]
                                                          theorem Complex.ofReal_cot_ofReal_re (x : ) :
                                                          (↑x).cot.re = (↑x).cot
                                                          @[simp]
                                                          theorem Complex.ofReal_tan (x : ) :
                                                          (Real.tan x) = tan x
                                                          @[simp]
                                                          theorem Complex.ofReal_cot (x : ) :
                                                          x.cot = (↑x).cot
                                                          @[simp]
                                                          theorem Complex.tan_ofReal_im (x : ) :
                                                          (tan x).im = 0
                                                          theorem Complex.cos_add_sin_I (x : ) :
                                                          cos x + sin x * I = exp (x * I)
                                                          theorem Complex.cos_sub_sin_I (x : ) :
                                                          cos x - sin x * I = exp (-x * I)
                                                          @[simp]
                                                          theorem Complex.sin_sq_add_cos_sq (x : ) :
                                                          sin x ^ 2 + cos x ^ 2 = 1
                                                          @[simp]
                                                          theorem Complex.cos_sq_add_sin_sq (x : ) :
                                                          cos x ^ 2 + sin x ^ 2 = 1
                                                          theorem Complex.cos_two_mul' (x : ) :
                                                          cos (2 * x) = cos x ^ 2 - sin x ^ 2
                                                          theorem Complex.cos_two_mul (x : ) :
                                                          cos (2 * x) = 2 * cos x ^ 2 - 1
                                                          theorem Complex.sin_two_mul (x : ) :
                                                          sin (2 * x) = 2 * sin x * cos x
                                                          theorem Complex.cos_sq (x : ) :
                                                          cos x ^ 2 = 1 / 2 + cos (2 * x) / 2
                                                          theorem Complex.cos_sq' (x : ) :
                                                          cos x ^ 2 = 1 - sin x ^ 2
                                                          theorem Complex.sin_sq (x : ) :
                                                          sin x ^ 2 = 1 - cos x ^ 2
                                                          theorem Complex.inv_one_add_tan_sq {x : } (hx : cos x 0) :
                                                          (1 + tan x ^ 2)⁻¹ = cos x ^ 2
                                                          theorem Complex.tan_sq_div_one_add_tan_sq {x : } (hx : cos x 0) :
                                                          tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2
                                                          theorem Complex.cos_three_mul (x : ) :
                                                          cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x
                                                          theorem Complex.sin_three_mul (x : ) :
                                                          sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
                                                          theorem Complex.exp_mul_I (x : ) :
                                                          exp (x * I) = cos x + sin x * I
                                                          theorem Complex.exp_add_mul_I (x y : ) :
                                                          exp (x + y * I) = exp x * (cos y + sin y * I)
                                                          theorem Complex.exp_eq_exp_re_mul_sin_add_cos (x : ) :
                                                          exp x = exp x.re * (cos x.im + sin x.im * I)
                                                          @[simp]
                                                          theorem Complex.exp_ofReal_mul_I_re (x : ) :
                                                          (exp (x * I)).re = Real.cos x
                                                          @[simp]
                                                          theorem Complex.exp_ofReal_mul_I_im (x : ) :
                                                          (exp (x * I)).im = Real.sin x
                                                          theorem Complex.cos_add_sin_mul_I_pow (n : ) (z : ) :
                                                          (cos z + sin z * I) ^ n = cos (n * z) + sin (n * z) * I

                                                          De Moivre's formula

                                                          @[simp]
                                                          theorem Real.sin_zero :
                                                          sin 0 = 0
                                                          @[simp]
                                                          theorem Real.sin_neg (x : ) :
                                                          sin (-x) = -sin x
                                                          theorem Real.sin_add (x y : ) :
                                                          sin (x + y) = sin x * cos y + cos x * sin y
                                                          @[simp]
                                                          theorem Real.cos_zero :
                                                          cos 0 = 1
                                                          @[simp]
                                                          theorem Real.cos_neg (x : ) :
                                                          cos (-x) = cos x
                                                          @[simp]
                                                          theorem Real.cos_abs (x : ) :
                                                          cos |x| = cos x
                                                          theorem Real.cos_add (x y : ) :
                                                          cos (x + y) = cos x * cos y - sin x * sin y
                                                          theorem Real.sin_sub (x y : ) :
                                                          sin (x - y) = sin x * cos y - cos x * sin y
                                                          theorem Real.cos_sub (x y : ) :
                                                          cos (x - y) = cos x * cos y + sin x * sin y
                                                          theorem Real.sin_sub_sin (x y : ) :
                                                          sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
                                                          theorem Real.cos_sub_cos (x y : ) :
                                                          cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
                                                          theorem Real.cos_add_cos (x y : ) :
                                                          cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
                                                          theorem Real.two_mul_sin_mul_sin (x y : ) :
                                                          2 * sin x * sin y = cos (x - y) - cos (x + y)
                                                          theorem Real.two_mul_cos_mul_cos (x y : ) :
                                                          2 * cos x * cos y = cos (x - y) + cos (x + y)
                                                          theorem Real.two_mul_sin_mul_cos (x y : ) :
                                                          2 * sin x * cos y = sin (x - y) + sin (x + y)
                                                          theorem Real.tan_mul_cos {x : } (hx : cos x 0) :
                                                          tan x * cos x = sin x
                                                          @[simp]
                                                          theorem Real.tan_zero :
                                                          tan 0 = 0
                                                          @[simp]
                                                          theorem Real.tan_neg (x : ) :
                                                          tan (-x) = -tan x
                                                          @[simp]
                                                          theorem Real.sin_sq_add_cos_sq (x : ) :
                                                          sin x ^ 2 + cos x ^ 2 = 1
                                                          @[simp]
                                                          theorem Real.cos_sq_add_sin_sq (x : ) :
                                                          cos x ^ 2 + sin x ^ 2 = 1
                                                          theorem Real.sin_sq_le_one (x : ) :
                                                          sin x ^ 2 1
                                                          theorem Real.cos_sq_le_one (x : ) :
                                                          cos x ^ 2 1
                                                          theorem Real.sin_le_one (x : ) :
                                                          sin x 1
                                                          theorem Real.cos_le_one (x : ) :
                                                          cos x 1
                                                          theorem Real.neg_one_le_sin (x : ) :
                                                          -1 sin x
                                                          theorem Real.neg_one_le_cos (x : ) :
                                                          -1 cos x
                                                          theorem Real.cos_two_mul (x : ) :
                                                          cos (2 * x) = 2 * cos x ^ 2 - 1
                                                          theorem Real.cos_two_mul' (x : ) :
                                                          cos (2 * x) = cos x ^ 2 - sin x ^ 2
                                                          theorem Real.sin_two_mul (x : ) :
                                                          sin (2 * x) = 2 * sin x * cos x
                                                          theorem Real.cos_sq (x : ) :
                                                          cos x ^ 2 = 1 / 2 + cos (2 * x) / 2
                                                          theorem Real.cos_sq' (x : ) :
                                                          cos x ^ 2 = 1 - sin x ^ 2
                                                          theorem Real.sin_sq (x : ) :
                                                          sin x ^ 2 = 1 - cos x ^ 2
                                                          theorem Real.sin_sq_eq_half_sub (x : ) :
                                                          sin x ^ 2 = 1 / 2 - cos (2 * x) / 2
                                                          theorem Real.inv_one_add_tan_sq {x : } (hx : cos x 0) :
                                                          (1 + tan x ^ 2)⁻¹ = cos x ^ 2
                                                          theorem Real.tan_sq_div_one_add_tan_sq {x : } (hx : cos x 0) :
                                                          tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2
                                                          theorem Real.inv_sqrt_one_add_tan_sq {x : } (hx : 0 < cos x) :
                                                          ((1 + tan x ^ 2))⁻¹ = cos x
                                                          theorem Real.tan_div_sqrt_one_add_tan_sq {x : } (hx : 0 < cos x) :
                                                          tan x / (1 + tan x ^ 2) = sin x
                                                          theorem Real.cos_three_mul (x : ) :
                                                          cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x
                                                          theorem Real.sin_three_mul (x : ) :
                                                          sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
                                                          theorem Real.sinh_eq (x : ) :
                                                          sinh x = (exp x - exp (-x)) / 2

                                                          The definition of sinh in terms of exp.

                                                          @[simp]
                                                          theorem Real.sinh_zero :
                                                          sinh 0 = 0
                                                          @[simp]
                                                          theorem Real.sinh_neg (x : ) :
                                                          sinh (-x) = -sinh x
                                                          theorem Real.sinh_add (x y : ) :
                                                          sinh (x + y) = sinh x * cosh y + cosh x * sinh y
                                                          theorem Real.cosh_eq (x : ) :
                                                          cosh x = (exp x + exp (-x)) / 2

                                                          The definition of cosh in terms of exp.

                                                          @[simp]
                                                          theorem Real.cosh_zero :
                                                          cosh 0 = 1
                                                          @[simp]
                                                          theorem Real.cosh_neg (x : ) :
                                                          cosh (-x) = cosh x
                                                          @[simp]
                                                          theorem Real.cosh_abs (x : ) :
                                                          theorem Real.cosh_add (x y : ) :
                                                          cosh (x + y) = cosh x * cosh y + sinh x * sinh y
                                                          theorem Real.sinh_sub (x y : ) :
                                                          sinh (x - y) = sinh x * cosh y - cosh x * sinh y
                                                          theorem Real.cosh_sub (x y : ) :
                                                          cosh (x - y) = cosh x * cosh y - sinh x * sinh y
                                                          @[simp]
                                                          theorem Real.tanh_zero :
                                                          tanh 0 = 0
                                                          @[simp]
                                                          theorem Real.tanh_neg (x : ) :
                                                          tanh (-x) = -tanh x
                                                          @[simp]
                                                          theorem Real.cosh_add_sinh (x : ) :
                                                          cosh x + sinh x = exp x
                                                          @[simp]
                                                          theorem Real.sinh_add_cosh (x : ) :
                                                          sinh x + cosh x = exp x
                                                          @[simp]
                                                          theorem Real.exp_sub_cosh (x : ) :
                                                          exp x - cosh x = sinh x
                                                          @[simp]
                                                          theorem Real.exp_sub_sinh (x : ) :
                                                          exp x - sinh x = cosh x
                                                          @[simp]
                                                          theorem Real.cosh_sub_sinh (x : ) :
                                                          cosh x - sinh x = exp (-x)
                                                          @[simp]
                                                          theorem Real.sinh_sub_cosh (x : ) :
                                                          sinh x - cosh x = -exp (-x)
                                                          @[simp]
                                                          theorem Real.cosh_sq_sub_sinh_sq (x : ) :
                                                          cosh x ^ 2 - sinh x ^ 2 = 1
                                                          theorem Real.cosh_sq (x : ) :
                                                          cosh x ^ 2 = sinh x ^ 2 + 1
                                                          theorem Real.cosh_sq' (x : ) :
                                                          cosh x ^ 2 = 1 + sinh x ^ 2
                                                          theorem Real.sinh_sq (x : ) :
                                                          sinh x ^ 2 = cosh x ^ 2 - 1
                                                          theorem Real.cosh_two_mul (x : ) :
                                                          cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2
                                                          theorem Real.sinh_two_mul (x : ) :
                                                          sinh (2 * x) = 2 * sinh x * cosh x
                                                          theorem Real.cosh_three_mul (x : ) :
                                                          cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
                                                          theorem Real.sinh_three_mul (x : ) :
                                                          sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x
                                                          theorem Real.cosh_pos (x : ) :
                                                          0 < cosh x

                                                          Real.cosh is always positive

                                                          theorem Real.cos_bound {x : } (hx : |x| 1) :
                                                          |cos x - (1 - x ^ 2 / 2)| |x| ^ 4 * (5 / 96)
                                                          theorem Real.sin_bound {x : } (hx : |x| 1) :
                                                          |sin x - (x - x ^ 3 / 6)| |x| ^ 4 * (5 / 96)
                                                          theorem Real.cos_pos_of_le_one {x : } (hx : |x| 1) :
                                                          0 < cos x
                                                          theorem Real.sin_pos_of_pos_of_le_one {x : } (hx0 : 0 < x) (hx : x 1) :
                                                          0 < sin x
                                                          theorem Real.sin_pos_of_pos_of_le_two {x : } (hx0 : 0 < x) (hx : x 2) :
                                                          0 < sin x
                                                          theorem Real.cos_one_le :
                                                          cos 1 5 / 9

                                                          Extension for the positivity tactic: Real.cosh is always positive.

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem Complex.norm_cos_add_sin_mul_I (x : ) :
                                                              cos x + sin x * I = 1
                                                              @[simp]
                                                              @[deprecated Complex.norm_cos_add_sin_mul_I (since := "2025-02-16")]
                                                              theorem Complex.abs_cos_add_sin_mul_I (x : ) :
                                                              cos x + sin x * I = 1

                                                              Alias of Complex.norm_cos_add_sin_mul_I.

                                                              @[deprecated Complex.norm_exp_ofReal_mul_I (since := "2025-02-16")]
                                                              theorem Complex.abs_exp_ofReal_mul_I (x : ) :
                                                              exp (x * I) = 1

                                                              Alias of Complex.norm_exp_ofReal_mul_I.

                                                              @[deprecated Complex.norm_exp (since := "2025-02-16")]

                                                              Alias of Complex.norm_exp.

                                                              @[deprecated Complex.norm_exp_eq_iff_re_eq (since := "2025-02-16")]

                                                              Alias of Complex.norm_exp_eq_iff_re_eq.