Documentation

Mathlib.Data.Complex.Basic

The complex numbers #

The complex numbers are modelled as ℝ^2 in the obvious way and it is shown that they form a field of characteristic zero. The result that the complex numbers are algebraically closed, see FieldTheory.AlgebraicClosure.

Definition and basic arithmetic #

structure Complex :

Complex numbers consist of two Reals: a real part re and an imaginary part im.

  • re :

    The real part of a complex number.

  • im :

    The imaginary part of a complex number.

Instances For

    Complex numbers consist of two Reals: a real part re and an imaginary part im.

    Equations
    Instances For

      The equivalence between the complex numbers and ℝ × ℝ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        @[simp]
        theorem Complex.eta (z : ) :
        { re := z.re, im := z.im } = z
        theorem Complex.ext {z w : } :
        z.re = w.rez.im = w.imz = w
        @[simp]
        @[simp]

        The natural inclusion of the real numbers into the complex numbers.

        Equations
        • r = { re := r, im := 0 }
        Instances For
          @[deprecated Complex.ofReal]

          Alias of Complex.ofReal.


          The natural inclusion of the real numbers into the complex numbers.

          Equations
          Instances For
            @[simp]
            theorem Complex.ofReal_re (r : ) :
            (↑r).re = r
            @[simp]
            theorem Complex.ofReal_im (r : ) :
            (↑r).im = 0
            theorem Complex.ofReal_def (r : ) :
            r = { re := r, im := 0 }
            @[simp]
            theorem Complex.ofReal_inj {z w : } :
            z = w z = w
            instance Complex.canLift :
            CanLift Complex.ofReal fun (z : ) => z.im = 0

            The product of a set on the real axis and a set on the imaginary axis of the complex plane, denoted by s ×ℂ t.

            Equations
            Instances For

              The product of a set on the real axis and a set on the imaginary axis of the complex plane, denoted by s ×ℂ t.

              Equations
              Instances For
                theorem Complex.mem_reProdIm {z : } {s t : Set } :
                z s ×ℂ t z.re s z.im t
                Equations
                @[simp]
                @[simp]
                @[simp]
                theorem Complex.ofReal_zero :
                0 = 0
                @[simp]
                theorem Complex.ofReal_eq_zero {z : } :
                z = 0 z = 0
                theorem Complex.ofReal_ne_zero {z : } :
                z 0 z 0
                Equations
                @[simp]
                @[simp]
                @[simp]
                theorem Complex.ofReal_one :
                1 = 1
                @[simp]
                theorem Complex.ofReal_eq_one {z : } :
                z = 1 z = 1
                theorem Complex.ofReal_ne_one {z : } :
                z 1 z 1
                Equations
                @[simp]
                theorem Complex.add_re (z w : ) :
                (z + w).re = z.re + w.re
                @[simp]
                theorem Complex.add_im (z w : ) :
                (z + w).im = z.im + w.im
                @[simp]
                theorem Complex.ofReal_add (r s : ) :
                (r + s) = r + s
                Equations
                @[simp]
                theorem Complex.neg_re (z : ) :
                (-z).re = -z.re
                @[simp]
                theorem Complex.neg_im (z : ) :
                (-z).im = -z.im
                @[simp]
                theorem Complex.ofReal_neg (r : ) :
                (-r) = -r
                Equations
                Equations
                @[simp]
                theorem Complex.mul_re (z w : ) :
                (z * w).re = z.re * w.re - z.im * w.im
                @[simp]
                theorem Complex.mul_im (z w : ) :
                (z * w).im = z.re * w.im + z.im * w.re
                @[simp]
                theorem Complex.ofReal_mul (r s : ) :
                (r * s) = r * s
                theorem Complex.re_ofReal_mul (r : ) (z : ) :
                (r * z).re = r * z.re
                theorem Complex.im_ofReal_mul (r : ) (z : ) :
                (r * z).im = r * z.im
                theorem Complex.re_mul_ofReal (z : ) (r : ) :
                (z * r).re = z.re * r
                theorem Complex.im_mul_ofReal (z : ) (r : ) :
                (z * r).im = z.im * r
                theorem Complex.ofReal_mul' (r : ) (z : ) :
                r * z = { re := r * z.re, im := r * z.im }

                The imaginary unit, I #

                The imaginary unit.

                Equations
                Instances For
                  @[simp]
                  theorem Complex.I_re :
                  @[simp]
                  theorem Complex.I_im :
                  theorem Complex.I_mul (z : ) :
                  Complex.I * z = { re := -z.im, im := z.re }
                  theorem Complex.mk_eq_add_mul_I (a b : ) :
                  { re := a, im := b } = a + b * Complex.I
                  @[simp]
                  theorem Complex.re_add_im (z : ) :
                  z.re + z.im * Complex.I = z
                  theorem Complex.mul_I_re (z : ) :
                  (z * Complex.I).re = -z.im
                  theorem Complex.mul_I_im (z : ) :
                  (z * Complex.I).im = z.re
                  theorem Complex.I_mul_re (z : ) :
                  (Complex.I * z).re = -z.im
                  theorem Complex.I_mul_im (z : ) :
                  (Complex.I * z).im = z.re

                  The natural AddEquiv from to ℝ × ℝ.

                  Equations
                  Instances For

                    Commutative ring instance and lemmas #

                    Scalar multiplication by R on extends to . This is used here and in Matlib.Data.Complex.Module to transfer instances from to , but is not needed outside, so we make it scoped.

                    Equations
                    • Complex.SMul.instSMulRealComplex = { smul := fun (r : R) (x : ) => { re := r x.re - 0 * x.im, im := r x.im + 0 * x.re } }
                    Instances For
                      theorem Complex.smul_re {R : Type u_1} [SMul R ] (r : R) (z : ) :
                      (r z).re = r z.re
                      theorem Complex.smul_im {R : Type u_1} [SMul R ] (r : R) (z : ) :
                      (r z).im = r z.im
                      @[simp]
                      theorem Complex.real_smul {x : } {z : } :
                      x z = x * z
                      Equations
                      • One or more equations did not get rendered due to their size.

                      This shortcut instance ensures we do not find Ring via the noncomputable Complex.field instance.

                      Equations

                      This shortcut instance ensures we do not find CommSemiring via the noncomputable Complex.field instance.

                      Equations

                      This shortcut instance ensures we do not find Semiring via the noncomputable Complex.field instance.

                      Equations

                      The "real part" map, considered as an additive group homomorphism.

                      Equations
                      Instances For

                        The "imaginary part" map, considered as an additive group homomorphism.

                        Equations
                        Instances For

                          Cast lemmas #

                          noncomputable instance Complex.instNNRatCast :
                          Equations
                          noncomputable instance Complex.instRatCast :
                          Equations
                          @[simp]
                          theorem Complex.ofReal_ofNat (n : ) [n.AtLeastTwo] :
                          @[simp]
                          theorem Complex.ofReal_natCast (n : ) :
                          n = n
                          @[simp]
                          theorem Complex.ofReal_intCast (n : ) :
                          n = n
                          @[simp]
                          theorem Complex.ofReal_nnratCast (q : ℚ≥0) :
                          q = q
                          @[simp]
                          theorem Complex.ofReal_ratCast (q : ) :
                          q = q
                          @[deprecated Complex.ofReal_ratCast]
                          theorem Complex.ofReal_rat_cast (q : ) :
                          q = q

                          Alias of Complex.ofReal_ratCast.

                          @[simp]
                          theorem Complex.re_ofNat (n : ) [n.AtLeastTwo] :
                          @[simp]
                          theorem Complex.im_ofNat (n : ) [n.AtLeastTwo] :
                          (OfNat.ofNat n).im = 0
                          @[simp]
                          theorem Complex.natCast_re (n : ) :
                          (↑n).re = n
                          @[simp]
                          theorem Complex.natCast_im (n : ) :
                          (↑n).im = 0
                          @[simp]
                          theorem Complex.intCast_re (n : ) :
                          (↑n).re = n
                          @[simp]
                          theorem Complex.intCast_im (n : ) :
                          (↑n).im = 0
                          @[simp]
                          theorem Complex.re_nnratCast (q : ℚ≥0) :
                          (↑q).re = q
                          @[simp]
                          theorem Complex.im_nnratCast (q : ℚ≥0) :
                          (↑q).im = 0
                          @[simp]
                          theorem Complex.ratCast_re (q : ) :
                          (↑q).re = q
                          @[simp]
                          theorem Complex.ratCast_im (q : ) :
                          (↑q).im = 0
                          theorem Complex.re_nsmul (n : ) (z : ) :
                          (n z).re = n z.re
                          theorem Complex.im_nsmul (n : ) (z : ) :
                          (n z).im = n z.im
                          theorem Complex.re_zsmul (n : ) (z : ) :
                          (n z).re = n z.re
                          theorem Complex.im_zsmul (n : ) (z : ) :
                          (n z).im = n z.im
                          @[simp]
                          theorem Complex.re_nnqsmul (q : ℚ≥0) (z : ) :
                          (q z).re = q z.re
                          @[simp]
                          theorem Complex.im_nnqsmul (q : ℚ≥0) (z : ) :
                          (q z).im = q z.im
                          @[simp]
                          theorem Complex.re_qsmul (q : ) (z : ) :
                          (q z).re = q z.re
                          @[simp]
                          theorem Complex.im_qsmul (q : ) (z : ) :
                          (q z).im = q z.im
                          @[deprecated Complex.ratCast_im]
                          theorem Complex.rat_cast_im (q : ) :
                          (↑q).im = 0

                          Alias of Complex.ratCast_im.

                          theorem Complex.ofReal_nsmul (n : ) (r : ) :
                          (n r) = n r
                          theorem Complex.ofReal_zsmul (n : ) (r : ) :
                          (n r) = n r

                          Complex conjugation #

                          This defines the complex conjugate as the star operation of the StarRing. It is recommended to use the ring endomorphism version starRingEnd, available under the notation conj in the locale ComplexConjugate.

                          Equations
                          @[simp]
                          theorem Complex.conj_re (z : ) :
                          ((starRingEnd ) z).re = z.re
                          @[simp]
                          theorem Complex.conj_im (z : ) :
                          ((starRingEnd ) z).im = -z.im
                          @[simp]
                          theorem Complex.conj_ofReal (r : ) :
                          (starRingEnd ) r = r
                          theorem Complex.conj_natCast (n : ) :
                          (starRingEnd ) n = n
                          @[deprecated Complex.conj_natCast]
                          theorem Complex.conj_nat_cast (n : ) :
                          (starRingEnd ) n = n

                          Alias of Complex.conj_natCast.

                          theorem Complex.conj_ofNat (n : ) [n.AtLeastTwo] :
                          theorem Complex.conj_eq_iff_real {z : } :
                          (starRingEnd ) z = z ∃ (r : ), z = r
                          theorem Complex.conj_eq_iff_re {z : } :
                          (starRingEnd ) z = z z.re = z
                          theorem Complex.conj_eq_iff_im {z : } :
                          (starRingEnd ) z = z z.im = 0
                          @[simp]
                          theorem Complex.star_def :
                          star = (starRingEnd )

                          Norm squared #

                          The norm squared function.

                          Equations
                          Instances For
                            theorem Complex.normSq_apply (z : ) :
                            Complex.normSq z = z.re * z.re + z.im * z.im
                            @[simp]
                            theorem Complex.normSq_ofReal (r : ) :
                            Complex.normSq r = r * r
                            @[simp]
                            theorem Complex.normSq_natCast (n : ) :
                            Complex.normSq n = n * n
                            @[deprecated Complex.normSq_natCast]
                            theorem Complex.normSq_nat_cast (n : ) :
                            Complex.normSq n = n * n

                            Alias of Complex.normSq_natCast.

                            @[simp]
                            theorem Complex.normSq_intCast (z : ) :
                            Complex.normSq z = z * z
                            @[deprecated Complex.normSq_intCast]
                            theorem Complex.normSq_int_cast (z : ) :
                            Complex.normSq z = z * z

                            Alias of Complex.normSq_intCast.

                            @[simp]
                            theorem Complex.normSq_ratCast (q : ) :
                            Complex.normSq q = q * q
                            @[deprecated Complex.normSq_ratCast]
                            theorem Complex.normSq_rat_cast (q : ) :
                            Complex.normSq q = q * q

                            Alias of Complex.normSq_ratCast.

                            @[simp]
                            @[simp]
                            theorem Complex.normSq_mk (x y : ) :
                            Complex.normSq { re := x, im := y } = x * x + y * y
                            theorem Complex.normSq_add_mul_I (x y : ) :
                            Complex.normSq (x + y * Complex.I) = x ^ 2 + y ^ 2
                            @[simp]
                            theorem Complex.normSq_pos {z : } :
                            theorem Complex.add_conj (z : ) :
                            z + (starRingEnd ) z = (2 * z.re)

                            The coercion ℝ → ℂ as a RingHom.

                            Equations
                            Instances For
                              @[simp]
                              theorem Complex.ofReal_comp_add {α : Type u_1} (f g : α) :
                              @[simp]
                              theorem Complex.ofReal_comp_sub {α : Type u_1} (f g : α) :
                              @[simp]
                              theorem Complex.ofReal_comp_neg {α : Type u_1} (f : α) :
                              theorem Complex.ofReal_comp_nsmul {α : Type u_1} (n : ) (f : α) :
                              theorem Complex.ofReal_comp_zsmul {α : Type u_1} (n : ) (f : α) :
                              @[simp]
                              theorem Complex.ofReal_comp_mul {α : Type u_1} (f g : α) :
                              @[simp]
                              theorem Complex.ofReal_comp_pow {α : Type u_1} (f : α) (n : ) :
                              @[simp]
                              theorem Complex.I_sq :
                              @[simp]
                              @[simp]
                              theorem Complex.sub_re (z w : ) :
                              (z - w).re = z.re - w.re
                              @[simp]
                              theorem Complex.sub_im (z w : ) :
                              (z - w).im = z.im - w.im
                              @[simp]
                              theorem Complex.ofReal_sub (r s : ) :
                              (r - s) = r - s
                              @[simp]
                              theorem Complex.ofReal_pow (r : ) (n : ) :
                              (r ^ n) = r ^ n
                              theorem Complex.sub_conj (z : ) :
                              z - (starRingEnd ) z = (2 * z.im) * Complex.I

                              Inversion #

                              noncomputable instance Complex.instInv :
                              Equations
                              @[simp]
                              theorem Complex.inv_re (z : ) :
                              z⁻¹.re = z.re / Complex.normSq z
                              @[simp]
                              theorem Complex.inv_im (z : ) :
                              @[simp]
                              theorem Complex.ofReal_inv (r : ) :
                              r⁻¹ = (↑r)⁻¹
                              theorem Complex.mul_inv_cancel {z : } (h : z 0) :
                              z * z⁻¹ = 1
                              theorem Complex.div_re (z w : ) :
                              (z / w).re = z.re * w.re / Complex.normSq w + z.im * w.im / Complex.normSq w
                              theorem Complex.div_im (z w : ) :
                              (z / w).im = z.im * w.re / Complex.normSq w - z.re * w.im / Complex.normSq w

                              Field instance and lemmas #

                              noncomputable instance Complex.instField :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[simp]
                              theorem Complex.ofReal_nnqsmul (q : ℚ≥0) (r : ) :
                              (q r) = q r
                              @[simp]
                              theorem Complex.ofReal_qsmul (q : ) (r : ) :
                              (q r) = q r
                              @[simp]
                              theorem Complex.ofReal_div (r s : ) :
                              (r / s) = r / s
                              @[simp]
                              theorem Complex.ofReal_zpow (r : ) (n : ) :
                              (r ^ n) = r ^ n
                              @[simp]
                              theorem Complex.div_I (z : ) :
                              theorem Complex.div_ofReal (z : ) (x : ) :
                              z / x = { re := z.re / x, im := z.im / x }
                              theorem Complex.div_natCast (z : ) (n : ) :
                              z / n = { re := z.re / n, im := z.im / n }
                              @[deprecated Complex.div_natCast]
                              theorem Complex.div_nat_cast (z : ) (n : ) :
                              z / n = { re := z.re / n, im := z.im / n }

                              Alias of Complex.div_natCast.

                              theorem Complex.div_intCast (z : ) (n : ) :
                              z / n = { re := z.re / n, im := z.im / n }
                              @[deprecated Complex.div_intCast]
                              theorem Complex.div_int_cast (z : ) (n : ) :
                              z / n = { re := z.re / n, im := z.im / n }

                              Alias of Complex.div_intCast.

                              theorem Complex.div_ratCast (z : ) (x : ) :
                              z / x = { re := z.re / x, im := z.im / x }
                              @[deprecated Complex.div_ratCast]
                              theorem Complex.div_rat_cast (z : ) (x : ) :
                              z / x = { re := z.re / x, im := z.im / x }

                              Alias of Complex.div_ratCast.

                              theorem Complex.div_ofNat (z : ) (n : ) [n.AtLeastTwo] :
                              z / OfNat.ofNat n = { re := z.re / OfNat.ofNat n, im := z.im / OfNat.ofNat n }
                              @[simp]
                              theorem Complex.div_ofReal_re (z : ) (x : ) :
                              (z / x).re = z.re / x
                              @[simp]
                              theorem Complex.div_ofReal_im (z : ) (x : ) :
                              (z / x).im = z.im / x
                              @[simp]
                              theorem Complex.div_natCast_re (z : ) (n : ) :
                              (z / n).re = z.re / n
                              @[simp]
                              theorem Complex.div_natCast_im (z : ) (n : ) :
                              (z / n).im = z.im / n
                              @[simp]
                              theorem Complex.div_intCast_re (z : ) (n : ) :
                              (z / n).re = z.re / n
                              @[simp]
                              theorem Complex.div_intCast_im (z : ) (n : ) :
                              (z / n).im = z.im / n
                              @[simp]
                              theorem Complex.div_ratCast_re (z : ) (x : ) :
                              (z / x).re = z.re / x
                              @[simp]
                              theorem Complex.div_ratCast_im (z : ) (x : ) :
                              (z / x).im = z.im / x
                              @[deprecated Complex.div_ratCast_im]
                              theorem Complex.div_rat_cast_im (z : ) (x : ) :
                              (z / x).im = z.im / x

                              Alias of Complex.div_ratCast_im.

                              @[simp]
                              theorem Complex.div_ofNat_re (z : ) (n : ) [n.AtLeastTwo] :
                              (z / OfNat.ofNat n).re = z.re / OfNat.ofNat n
                              @[simp]
                              theorem Complex.div_ofNat_im (z : ) (n : ) [n.AtLeastTwo] :
                              (z / OfNat.ofNat n).im = z.im / OfNat.ofNat n

                              Characteristic zero #

                              theorem Complex.re_eq_add_conj (z : ) :
                              z.re = (z + (starRingEnd ) z) / 2

                              A complex number z plus its conjugate conj z is 2 times its real part.

                              theorem Complex.im_eq_sub_conj (z : ) :
                              z.im = (z - (starRingEnd ) z) / (2 * Complex.I)

                              A complex number z minus its conjugate conj z is 2i times its imaginary part.

                              unsafe instance Complex.instRepr :

                              Show the imaginary number ⟨x, y⟩ as an "x + y*I" string

                              Note that the Real numbers used for x and y will show as cauchy sequences due to the way Real numbers are represented.

                              Equations
                              • One or more equations did not get rendered due to their size.

                              The preimage under equivRealProd of s ×ˢ t is s ×ℂ t.

                              theorem Complex.reProdIm_subset_iff {s s₁ t t₁ : Set } :
                              s ×ℂ t s₁ ×ℂ t₁ s ×ˢ t s₁ ×ˢ t₁

                              The inequality s × t ⊆ s₁ × t₁ holds in iff it holds in ℝ × ℝ.

                              theorem Complex.reProdIm_subset_iff' {s s₁ t t₁ : Set } :
                              s ×ℂ t s₁ ×ℂ t₁ s s₁ t t₁ s = t =

                              If s ⊆ s₁ ⊆ ℝ and t ⊆ t₁ ⊆ ℝ, then s × t ⊆ s₁ × t₁ in .

                              A Rectangle is an axis-parallel rectangle with corners z and w.

                              Equations
                              Instances For
                                theorem Complex.horizontalSegment_eq (a₁ a₂ b : ) :
                                (fun (x : ) => x + b * Complex.I) '' Set.uIcc a₁ a₂ = Set.uIcc a₁ a₂ ×ℂ {b}

                                A real segment [a₁, a₂] translated by b * I is the complex line segment.

                                theorem Complex.verticalSegment_eq (a b₁ b₂ : ) :
                                (fun (y : ) => a + y * Complex.I) '' Set.uIcc b₁ b₂ = {a} ×ℂ Set.uIcc b₁ b₂

                                A vertical segment [b₁, b₂] translated by a is the complex line segment.