Documentation

Mathlib.Data.IsROrC.Basic

IsROrC: a typeclass for ℝ or ℂ #

This file defines the typeclass IsROrC intended to have only two instances: ℝ and ℂ. It is meant for definitions and theorems which hold for both the real and the complex case, and in particular when the real case follows directly from the complex case by setting re to id, im to zero and so on. Its API follows closely that of ℂ.

Applications include defining inner products and Hilbert spaces for both the real and complex case. One typically produces the definitions and proof for an arbitrary field of this typeclass, which basically amounts to doing the complex case, and the two cases then fall out immediately from the two instances of the class.

The instance for is registered in this file. The instance for is declared in Mathlib/Analysis/Complex/Basic.lean.

Implementation notes #

The coercion from reals into an IsROrC field is done by registering IsROrC.ofReal as a CoeTC. For this to work, we must proceed carefully to avoid problems involving circular coercions in the case K=ℝ; in particular, we cannot use the plain Coe and must set priorities carefully. This problem was already solved for , and we copy the solution detailed in Mathlib/Data/Nat/Cast/Defs.lean. See also Note [coercion into rings] for more details.

In addition, several lemmas need to be set at priority 900 to make sure that they do not override their counterparts in Mathlib/Analysis/Complex/Basic.lean (which causes linter errors).

A few lemmas requiring heavier imports are in Mathlib/Data/IsROrC/Lemmas.lean.

This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.

Instances
    @[inline, reducible]
    abbrev IsROrC.ofReal {K : Type u_1} [IsROrC K] :
    K

    Coercion from to an IsROrC field.

    Equations
    • IsROrC.ofReal = Algebra.cast
    Instances For
      noncomputable instance IsROrC.algebraMapCoe {K : Type u_1} [IsROrC K] :
      Equations
      • IsROrC.algebraMapCoe = { coe := IsROrC.ofReal }
      theorem IsROrC.ofReal_alg {K : Type u_1} [IsROrC K] (x : ) :
      x = x 1
      theorem IsROrC.real_smul_eq_coe_mul {K : Type u_1} [IsROrC K] (r : ) (z : K) :
      r z = r * z
      theorem IsROrC.real_smul_eq_coe_smul {K : Type u_1} {E : Type u_2} [IsROrC K] [AddCommGroup E] [Module K E] [Module E] [IsScalarTower K E] (r : ) (x : E) :
      r x = r x
      theorem IsROrC.algebraMap_eq_ofReal {K : Type u_1} [IsROrC K] :
      (algebraMap K) = IsROrC.ofReal
      @[simp]
      theorem IsROrC.re_add_im {K : Type u_1} [IsROrC K] (z : K) :
      (IsROrC.re z) + (IsROrC.im z) * IsROrC.I = z
      @[simp]
      theorem IsROrC.ofReal_re {K : Type u_1} [IsROrC K] (r : ) :
      IsROrC.re r = r
      @[simp]
      theorem IsROrC.ofReal_im {K : Type u_1} [IsROrC K] (r : ) :
      IsROrC.im r = 0
      @[simp]
      theorem IsROrC.mul_re {K : Type u_1} [IsROrC K] (z : K) (w : K) :
      IsROrC.re (z * w) = IsROrC.re z * IsROrC.re w - IsROrC.im z * IsROrC.im w
      @[simp]
      theorem IsROrC.mul_im {K : Type u_1} [IsROrC K] (z : K) (w : K) :
      IsROrC.im (z * w) = IsROrC.re z * IsROrC.im w + IsROrC.im z * IsROrC.re w
      theorem IsROrC.ext_iff {K : Type u_1} [IsROrC K] {z : K} {w : K} :
      z = w IsROrC.re z = IsROrC.re w IsROrC.im z = IsROrC.im w
      theorem IsROrC.ext {K : Type u_1} [IsROrC K] {z : K} {w : K} (hre : IsROrC.re z = IsROrC.re w) (him : IsROrC.im z = IsROrC.im w) :
      z = w
      theorem IsROrC.ofReal_zero {K : Type u_1} [IsROrC K] :
      0 = 0
      theorem IsROrC.zero_re' {K : Type u_1} [IsROrC K] :
      IsROrC.re 0 = 0
      theorem IsROrC.ofReal_one {K : Type u_1} [IsROrC K] :
      1 = 1
      @[simp]
      theorem IsROrC.one_re {K : Type u_1} [IsROrC K] :
      IsROrC.re 1 = 1
      @[simp]
      theorem IsROrC.one_im {K : Type u_1} [IsROrC K] :
      IsROrC.im 1 = 0
      theorem IsROrC.ofReal_injective {K : Type u_1} [IsROrC K] :
      Function.Injective IsROrC.ofReal
      theorem IsROrC.ofReal_inj {K : Type u_1} [IsROrC K] {z : } {w : } :
      z = w z = w
      @[deprecated]
      theorem IsROrC.bit0_re {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.re (bit0 z) = bit0 (IsROrC.re z)
      @[simp, deprecated]
      theorem IsROrC.bit1_re {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.re (bit1 z) = bit1 (IsROrC.re z)
      @[deprecated]
      theorem IsROrC.bit0_im {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.im (bit0 z) = bit0 (IsROrC.im z)
      @[simp, deprecated]
      theorem IsROrC.bit1_im {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.im (bit1 z) = bit0 (IsROrC.im z)
      theorem IsROrC.ofReal_eq_zero {K : Type u_1} [IsROrC K] {x : } :
      x = 0 x = 0
      theorem IsROrC.ofReal_ne_zero {K : Type u_1} [IsROrC K] {x : } :
      x 0 x 0
      @[simp]
      theorem IsROrC.ofReal_add {K : Type u_1} [IsROrC K] (r : ) (s : ) :
      (r + s) = r + s
      @[simp, deprecated]
      theorem IsROrC.ofReal_bit0 {K : Type u_1} [IsROrC K] (r : ) :
      (bit0 r) = bit0 r
      @[simp, deprecated]
      theorem IsROrC.ofReal_bit1 {K : Type u_1} [IsROrC K] (r : ) :
      (bit1 r) = bit1 r
      @[simp]
      theorem IsROrC.ofReal_neg {K : Type u_1} [IsROrC K] (r : ) :
      (-r) = -r
      @[simp]
      theorem IsROrC.ofReal_sub {K : Type u_1} [IsROrC K] (r : ) (s : ) :
      (r - s) = r - s
      @[simp]
      theorem IsROrC.ofReal_sum {K : Type u_1} [IsROrC K] {α : Type u_3} (s : Finset α) (f : α) :
      (Finset.sum s fun (i : α) => f i) = Finset.sum s fun (i : α) => (f i)
      @[simp]
      theorem IsROrC.ofReal_finsupp_sum {K : Type u_1} [IsROrC K] {α : Type u_3} {M : Type u_4} [Zero M] (f : α →₀ M) (g : αM) :
      (Finsupp.sum f fun (a : α) (b : M) => g a b) = Finsupp.sum f fun (a : α) (b : M) => (g a b)
      @[simp]
      theorem IsROrC.ofReal_mul {K : Type u_1} [IsROrC K] (r : ) (s : ) :
      (r * s) = r * s
      @[simp]
      theorem IsROrC.ofReal_pow {K : Type u_1} [IsROrC K] (r : ) (n : ) :
      (r ^ n) = r ^ n
      @[simp]
      theorem IsROrC.ofReal_prod {K : Type u_1} [IsROrC K] {α : Type u_3} (s : Finset α) (f : α) :
      (Finset.prod s fun (i : α) => f i) = Finset.prod s fun (i : α) => (f i)
      @[simp]
      theorem IsROrC.ofReal_finsupp_prod {K : Type u_1} [IsROrC K] {α : Type u_3} {M : Type u_4} [Zero M] (f : α →₀ M) (g : αM) :
      (Finsupp.prod f fun (a : α) (b : M) => g a b) = Finsupp.prod f fun (a : α) (b : M) => (g a b)
      @[simp]
      theorem IsROrC.real_smul_ofReal {K : Type u_1} [IsROrC K] (r : ) (x : ) :
      r x = r * x
      theorem IsROrC.re_ofReal_mul {K : Type u_1} [IsROrC K] (r : ) (z : K) :
      IsROrC.re (r * z) = r * IsROrC.re z
      theorem IsROrC.im_ofReal_mul {K : Type u_1} [IsROrC K] (r : ) (z : K) :
      IsROrC.im (r * z) = r * IsROrC.im z
      theorem IsROrC.smul_re {K : Type u_1} [IsROrC K] (r : ) (z : K) :
      IsROrC.re (r z) = r * IsROrC.re z
      theorem IsROrC.smul_im {K : Type u_1} [IsROrC K] (r : ) (z : K) :
      IsROrC.im (r z) = r * IsROrC.im z
      @[simp]
      theorem IsROrC.norm_ofReal {K : Type u_1} [IsROrC K] (r : ) :
      r = |r|

      Characteristic zero #

      instance IsROrC.charZero_isROrC {K : Type u_1} [IsROrC K] :

      ℝ and ℂ are both of characteristic zero.

      Equations
      • =

      The imaginary unit, I #

      @[simp]
      theorem IsROrC.I_re {K : Type u_1} [IsROrC K] :
      IsROrC.re IsROrC.I = 0

      The imaginary unit.

      @[simp]
      theorem IsROrC.I_im {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.im z * IsROrC.im IsROrC.I = IsROrC.im z
      @[simp]
      theorem IsROrC.I_im' {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.im IsROrC.I * IsROrC.im z = IsROrC.im z
      theorem IsROrC.I_mul_re {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.re (IsROrC.I * z) = -IsROrC.im z
      theorem IsROrC.I_mul_I {K : Type u_1} [IsROrC K] :
      IsROrC.I = 0 IsROrC.I * IsROrC.I = -1
      theorem IsROrC.I_eq_zero_or_im_I_eq_one {K : Type u_1} [IsROrC K] :
      IsROrC.I = 0 IsROrC.im IsROrC.I = 1
      @[simp]
      theorem IsROrC.conj_re {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.re ((starRingEnd K) z) = IsROrC.re z
      @[simp]
      theorem IsROrC.conj_im {K : Type u_1} [IsROrC K] (z : K) :
      IsROrC.im ((starRingEnd K) z) = -IsROrC.im z
      @[simp]
      theorem IsROrC.conj_I {K : Type u_1} [IsROrC K] :
      (starRingEnd K) IsROrC.I = -IsROrC.I
      @[simp]
      theorem IsROrC.conj_ofReal {K : Type u_1} [IsROrC K] (r : ) :
      (starRingEnd K) r = r
      @[deprecated]
      theorem IsROrC.conj_bit0 {K : Type u_1} [IsROrC K] (z : K) :
      @[deprecated]
      theorem IsROrC.conj_bit1 {K : Type u_1} [IsROrC K] (z : K) :
      theorem IsROrC.conj_neg_I {K : Type u_1} [IsROrC K] :
      (starRingEnd K) (-IsROrC.I) = IsROrC.I
      theorem IsROrC.conj_eq_re_sub_im {K : Type u_1} [IsROrC K] (z : K) :
      (starRingEnd K) z = (IsROrC.re z) - (IsROrC.im z) * IsROrC.I
      theorem IsROrC.sub_conj {K : Type u_1} [IsROrC K] (z : K) :
      z - (starRingEnd K) z = 2 * (IsROrC.im z) * IsROrC.I
      theorem IsROrC.conj_smul {K : Type u_1} [IsROrC K] (r : ) (z : K) :
      (starRingEnd K) (r z) = r (starRingEnd K) z
      theorem IsROrC.add_conj {K : Type u_1} [IsROrC K] (z : K) :
      z + (starRingEnd K) z = 2 * (IsROrC.re z)
      theorem IsROrC.re_eq_add_conj {K : Type u_1} [IsROrC K] (z : K) :
      (IsROrC.re z) = (z + (starRingEnd K) z) / 2
      theorem IsROrC.im_eq_conj_sub {K : Type u_1} [IsROrC K] (z : K) :
      (IsROrC.im z) = IsROrC.I * ((starRingEnd K) z - z) / 2
      theorem IsROrC.is_real_TFAE {K : Type u_1} [IsROrC K] (z : K) :
      List.TFAE [(starRingEnd K) z = z, ∃ (r : ), r = z, (IsROrC.re z) = z, IsROrC.im z = 0]

      There are several equivalent ways to say that a number z is in fact a real number.

      theorem IsROrC.conj_eq_iff_real {K : Type u_1} [IsROrC K] {z : K} :
      (starRingEnd K) z = z ∃ (r : ), z = r
      theorem IsROrC.conj_eq_iff_re {K : Type u_1} [IsROrC K] {z : K} :
      (starRingEnd K) z = z (IsROrC.re z) = z
      theorem IsROrC.conj_eq_iff_im {K : Type u_1} [IsROrC K] {z : K} :
      (starRingEnd K) z = z IsROrC.im z = 0
      @[simp]
      theorem IsROrC.star_def {K : Type u_1} [IsROrC K] :
      star = (starRingEnd K)
      @[inline, reducible]

      Conjugation as a ring equivalence. This is used to convert the inner product into a sesquilinear product.

      Equations
      Instances For
        def IsROrC.normSq {K : Type u_1} [IsROrC K] :

        The norm squared function.

        Equations
        • IsROrC.normSq = { toZeroHom := { toFun := fun (z : K) => IsROrC.re z * IsROrC.re z + IsROrC.im z * IsROrC.im z, map_zero' := }, map_one' := , map_mul' := }
        Instances For
          theorem IsROrC.normSq_apply {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.normSq z = IsROrC.re z * IsROrC.re z + IsROrC.im z * IsROrC.im z
          theorem IsROrC.norm_sq_eq_def {K : Type u_1} [IsROrC K] {z : K} :
          z ^ 2 = IsROrC.re z * IsROrC.re z + IsROrC.im z * IsROrC.im z
          theorem IsROrC.normSq_eq_def' {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.normSq z = z ^ 2
          theorem IsROrC.normSq_zero {K : Type u_1} [IsROrC K] :
          IsROrC.normSq 0 = 0
          theorem IsROrC.normSq_one {K : Type u_1} [IsROrC K] :
          IsROrC.normSq 1 = 1
          theorem IsROrC.normSq_nonneg {K : Type u_1} [IsROrC K] (z : K) :
          0 IsROrC.normSq z
          theorem IsROrC.normSq_eq_zero {K : Type u_1} [IsROrC K] {z : K} :
          IsROrC.normSq z = 0 z = 0
          @[simp]
          theorem IsROrC.normSq_pos {K : Type u_1} [IsROrC K] {z : K} :
          0 < IsROrC.normSq z z 0
          @[simp]
          theorem IsROrC.normSq_neg {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.normSq (-z) = IsROrC.normSq z
          @[simp]
          theorem IsROrC.normSq_conj {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.normSq ((starRingEnd K) z) = IsROrC.normSq z
          theorem IsROrC.normSq_mul {K : Type u_1} [IsROrC K] (z : K) (w : K) :
          IsROrC.normSq (z * w) = IsROrC.normSq z * IsROrC.normSq w
          theorem IsROrC.normSq_add {K : Type u_1} [IsROrC K] (z : K) (w : K) :
          IsROrC.normSq (z + w) = IsROrC.normSq z + IsROrC.normSq w + 2 * IsROrC.re (z * (starRingEnd K) w)
          theorem IsROrC.re_sq_le_normSq {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.re z * IsROrC.re z IsROrC.normSq z
          theorem IsROrC.im_sq_le_normSq {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.im z * IsROrC.im z IsROrC.normSq z
          theorem IsROrC.mul_conj {K : Type u_1} [IsROrC K] (z : K) :
          z * (starRingEnd K) z = z ^ 2
          theorem IsROrC.conj_mul {K : Type u_1} [IsROrC K] (z : K) :
          (starRingEnd K) z * z = z ^ 2
          theorem IsROrC.inv_eq_conj {K : Type u_1} [IsROrC K] {z : K} (hz : z = 1) :
          theorem IsROrC.normSq_sub {K : Type u_1} [IsROrC K] (z : K) (w : K) :
          IsROrC.normSq (z - w) = IsROrC.normSq z + IsROrC.normSq w - 2 * IsROrC.re (z * (starRingEnd K) w)
          theorem IsROrC.sqrt_normSq_eq_norm {K : Type u_1} [IsROrC K] {z : K} :
          Real.sqrt (IsROrC.normSq z) = z

          Inversion #

          @[simp]
          theorem IsROrC.ofReal_inv {K : Type u_1} [IsROrC K] (r : ) :
          r⁻¹ = (r)⁻¹
          theorem IsROrC.inv_def {K : Type u_1} [IsROrC K] (z : K) :
          z⁻¹ = (starRingEnd K) z * (z ^ 2)⁻¹
          @[simp]
          theorem IsROrC.inv_re {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.re z⁻¹ = IsROrC.re z / IsROrC.normSq z
          @[simp]
          theorem IsROrC.inv_im {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.im z⁻¹ = -IsROrC.im z / IsROrC.normSq z
          theorem IsROrC.div_re {K : Type u_1} [IsROrC K] (z : K) (w : K) :
          IsROrC.re (z / w) = IsROrC.re z * IsROrC.re w / IsROrC.normSq w + IsROrC.im z * IsROrC.im w / IsROrC.normSq w
          theorem IsROrC.div_im {K : Type u_1} [IsROrC K] (z : K) (w : K) :
          IsROrC.im (z / w) = IsROrC.im z * IsROrC.re w / IsROrC.normSq w - IsROrC.re z * IsROrC.im w / IsROrC.normSq w
          theorem IsROrC.conj_inv {K : Type u_1} [IsROrC K] (x : K) :
          theorem IsROrC.conj_div {K : Type u_1} [IsROrC K] (x : K) (y : K) :
          (starRingEnd K) (x / y) = (starRingEnd K) x / (starRingEnd K) y
          theorem IsROrC.exists_norm_eq_mul_self {K : Type u_1} [IsROrC K] (x : K) :
          ∃ (c : K), c = 1 x = c * x
          theorem IsROrC.exists_norm_mul_eq_self {K : Type u_1} [IsROrC K] (x : K) :
          ∃ (c : K), c = 1 c * x = x
          @[simp]
          theorem IsROrC.ofReal_div {K : Type u_1} [IsROrC K] (r : ) (s : ) :
          (r / s) = r / s
          theorem IsROrC.div_re_ofReal {K : Type u_1} [IsROrC K] {z : K} {r : } :
          IsROrC.re (z / r) = IsROrC.re z / r
          @[simp]
          theorem IsROrC.ofReal_zpow {K : Type u_1} [IsROrC K] (r : ) (n : ) :
          (r ^ n) = r ^ n
          theorem IsROrC.I_mul_I_of_nonzero {K : Type u_1} [IsROrC K] :
          IsROrC.I 0IsROrC.I * IsROrC.I = -1
          @[simp]
          theorem IsROrC.inv_I {K : Type u_1} [IsROrC K] :
          IsROrC.I⁻¹ = -IsROrC.I
          @[simp]
          theorem IsROrC.div_I {K : Type u_1} [IsROrC K] (z : K) :
          z / IsROrC.I = -(z * IsROrC.I)
          theorem IsROrC.normSq_inv {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.normSq z⁻¹ = (IsROrC.normSq z)⁻¹
          theorem IsROrC.normSq_div {K : Type u_1} [IsROrC K] (z : K) (w : K) :
          IsROrC.normSq (z / w) = IsROrC.normSq z / IsROrC.normSq w
          theorem IsROrC.norm_conj {K : Type u_1} [IsROrC K] {z : K} :

          Cast lemmas #

          @[simp]
          theorem IsROrC.ofReal_natCast {K : Type u_1} [IsROrC K] (n : ) :
          n = n
          @[simp]
          theorem IsROrC.natCast_re {K : Type u_1} [IsROrC K] (n : ) :
          IsROrC.re n = n
          @[simp]
          theorem IsROrC.natCast_im {K : Type u_1} [IsROrC K] (n : ) :
          IsROrC.im n = 0
          @[simp]
          theorem IsROrC.ofNat_re {K : Type u_1} [IsROrC K] (n : ) [Nat.AtLeastTwo n] :
          IsROrC.re (OfNat.ofNat n) = OfNat.ofNat n
          @[simp]
          theorem IsROrC.ofNat_im {K : Type u_1} [IsROrC K] (n : ) [Nat.AtLeastTwo n] :
          IsROrC.im (OfNat.ofNat n) = 0
          @[simp]
          theorem IsROrC.ofReal_ofNat {K : Type u_1} [IsROrC K] (n : ) [Nat.AtLeastTwo n] :
          theorem IsROrC.ofNat_mul_re {K : Type u_1} [IsROrC K] (n : ) [Nat.AtLeastTwo n] (z : K) :
          IsROrC.re (OfNat.ofNat n * z) = OfNat.ofNat n * IsROrC.re z
          theorem IsROrC.ofNat_mul_im {K : Type u_1} [IsROrC K] (n : ) [Nat.AtLeastTwo n] (z : K) :
          IsROrC.im (OfNat.ofNat n * z) = OfNat.ofNat n * IsROrC.im z
          @[simp]
          theorem IsROrC.ofReal_intCast {K : Type u_1} [IsROrC K] (n : ) :
          n = n
          @[simp]
          theorem IsROrC.intCast_re {K : Type u_1} [IsROrC K] (n : ) :
          IsROrC.re n = n
          @[simp]
          theorem IsROrC.intCast_im {K : Type u_1} [IsROrC K] (n : ) :
          IsROrC.im n = 0
          @[simp]
          theorem IsROrC.ofReal_ratCast {K : Type u_1} [IsROrC K] (n : ) :
          n = n
          @[simp]
          theorem IsROrC.ratCast_re {K : Type u_1} [IsROrC K] (q : ) :
          IsROrC.re q = q
          @[simp]
          theorem IsROrC.ratCast_im {K : Type u_1} [IsROrC K] (q : ) :
          IsROrC.im q = 0

          Norm #

          theorem IsROrC.norm_of_nonneg {K : Type u_1} [IsROrC K] {r : } (h : 0 r) :
          r = r
          @[simp]
          theorem IsROrC.norm_natCast {K : Type u_1} [IsROrC K] (n : ) :
          n = n
          theorem IsROrC.norm_nsmul (K : Type u_1) {E : Type u_2} [IsROrC K] [NormedAddCommGroup E] [NormedSpace K E] (n : ) (x : E) :
          theorem IsROrC.mul_self_norm {K : Type u_1} [IsROrC K] (z : K) :
          z * z = IsROrC.normSq z
          theorem IsROrC.norm_two {K : Type u_1} [IsROrC K] :
          theorem IsROrC.abs_re_le_norm {K : Type u_1} [IsROrC K] (z : K) :
          |IsROrC.re z| z
          theorem IsROrC.abs_im_le_norm {K : Type u_1} [IsROrC K] (z : K) :
          |IsROrC.im z| z
          theorem IsROrC.norm_re_le_norm {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.re z z
          theorem IsROrC.norm_im_le_norm {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.im z z
          theorem IsROrC.re_le_norm {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.re z z
          theorem IsROrC.im_le_norm {K : Type u_1} [IsROrC K] (z : K) :
          IsROrC.im z z
          theorem IsROrC.im_eq_zero_of_le {K : Type u_1} [IsROrC K] {a : K} (h : a IsROrC.re a) :
          IsROrC.im a = 0
          theorem IsROrC.re_eq_self_of_le {K : Type u_1} [IsROrC K] {a : K} (h : a IsROrC.re a) :
          (IsROrC.re a) = a
          theorem IsROrC.abs_re_div_norm_le_one {K : Type u_1} [IsROrC K] (z : K) :
          |IsROrC.re z / z| 1
          theorem IsROrC.abs_im_div_norm_le_one {K : Type u_1} [IsROrC K] (z : K) :
          |IsROrC.im z / z| 1
          theorem IsROrC.norm_I_of_ne_zero {K : Type u_1} [IsROrC K] (hI : IsROrC.I 0) :
          IsROrC.I = 1
          theorem IsROrC.re_eq_norm_of_mul_conj {K : Type u_1} [IsROrC K] (x : K) :
          IsROrC.re (x * (starRingEnd K) x) = x * (starRingEnd K) x
          theorem IsROrC.norm_sq_re_add_conj {K : Type u_1} [IsROrC K] (x : K) :
          x + (starRingEnd K) x ^ 2 = IsROrC.re (x + (starRingEnd K) x) ^ 2
          theorem IsROrC.norm_sq_re_conj_add {K : Type u_1} [IsROrC K] (x : K) :
          (starRingEnd K) x + x ^ 2 = IsROrC.re ((starRingEnd K) x + x) ^ 2

          Cauchy sequences #

          theorem IsROrC.isCauSeq_re {K : Type u_1} [IsROrC K] (f : CauSeq K norm) :
          IsCauSeq abs fun (n : ) => IsROrC.re (f n)
          theorem IsROrC.isCauSeq_im {K : Type u_1} [IsROrC K] (f : CauSeq K norm) :
          IsCauSeq abs fun (n : ) => IsROrC.im (f n)
          noncomputable def IsROrC.cauSeqRe {K : Type u_1} [IsROrC K] (f : CauSeq K norm) :

          The real part of a K Cauchy sequence, as a real Cauchy sequence.

          Equations
          Instances For
            noncomputable def IsROrC.cauSeqIm {K : Type u_1} [IsROrC K] (f : CauSeq K norm) :

            The imaginary part of a K Cauchy sequence, as a real Cauchy sequence.

            Equations
            Instances For
              theorem IsROrC.isCauSeq_norm {K : Type u_1} [IsROrC K] {f : K} (hf : IsCauSeq norm f) :
              IsCauSeq abs (norm f)
              noncomputable instance Real.isROrC :
              Equations
              • One or more equations did not get rendered due to their size.
              theorem IsROrC.lt_iff_re_im {K : Type u_1} [IsROrC K] {z : K} {w : K} :
              z < w IsROrC.re z < IsROrC.re w IsROrC.im z = IsROrC.im w
              theorem IsROrC.nonneg_iff {K : Type u_1} [IsROrC K] {z : K} :
              0 z 0 IsROrC.re z IsROrC.im z = 0
              theorem IsROrC.pos_iff {K : Type u_1} [IsROrC K] {z : K} :
              0 < z 0 < IsROrC.re z IsROrC.im z = 0
              theorem IsROrC.nonpos_iff {K : Type u_1} [IsROrC K] {z : K} :
              z 0 IsROrC.re z 0 IsROrC.im z = 0
              theorem IsROrC.neg_iff {K : Type u_1} [IsROrC K] {z : K} :
              z < 0 IsROrC.re z < 0 IsROrC.im z = 0
              theorem IsROrC.nonneg_iff_exists_ofReal {K : Type u_1} [IsROrC K] {z : K} :
              0 z ∃ x ≥ 0, x = z
              theorem IsROrC.pos_iff_exists_ofReal {K : Type u_1} [IsROrC K] {z : K} :
              0 < z ∃ x > 0, x = z
              theorem IsROrC.nonpos_iff_exists_ofReal {K : Type u_1} [IsROrC K] {z : K} :
              z 0 ∃ x ≤ 0, x = z
              theorem IsROrC.neg_iff_exists_ofReal {K : Type u_1} [IsROrC K] {z : K} :
              z < 0 ∃ x < 0, x = z

              With z ≤ w iff w - z is real and nonnegative, and are star ordered rings. (That is, a star ring in which the nonnegative elements are those of the form star z * z.)

              Note this is only an instance with open scoped ComplexOrder.

              Equations
              Instances For

                With z ≤ w iff w - z is real and nonnegative, and are strictly ordered rings.

                Note this is only an instance with open scoped ComplexOrder.

                Equations
                Instances For
                  @[simp]
                  theorem IsROrC.re_to_real {x : } :
                  IsROrC.re x = x
                  @[simp]
                  theorem IsROrC.im_to_real {x : } :
                  IsROrC.im x = 0
                  @[simp]
                  theorem IsROrC.I_to_real :
                  IsROrC.I = 0
                  @[simp]
                  theorem IsROrC.normSq_to_real {x : } :
                  IsROrC.normSq x = x * x
                  @[simp]
                  theorem IsROrC.ofReal_real_eq_id :
                  IsROrC.ofReal = id
                  def IsROrC.reLm {K : Type u_1} [IsROrC K] :

                  The real part in an IsROrC field, as a linear map.

                  Equations
                  • IsROrC.reLm = let __src := IsROrC.re; { toAddHom := { toFun := __src.toFun, map_add' := }, map_smul' := }
                  Instances For
                    @[simp]
                    theorem IsROrC.reLm_coe {K : Type u_1} [IsROrC K] :
                    IsROrC.reLm = IsROrC.re
                    noncomputable def IsROrC.reCLM {K : Type u_1} [IsROrC K] :

                    The real part in an IsROrC field, as a continuous linear map.

                    Equations
                    Instances For
                      @[simp]
                      theorem IsROrC.reCLM_coe {K : Type u_1} [IsROrC K] :
                      IsROrC.reCLM = IsROrC.reLm
                      @[simp]
                      theorem IsROrC.reCLM_apply {K : Type u_1} [IsROrC K] :
                      IsROrC.reCLM = IsROrC.re
                      theorem IsROrC.continuous_re {K : Type u_1} [IsROrC K] :
                      Continuous IsROrC.re
                      def IsROrC.imLm {K : Type u_1} [IsROrC K] :

                      The imaginary part in an IsROrC field, as a linear map.

                      Equations
                      • IsROrC.imLm = let __src := IsROrC.im; { toAddHom := { toFun := __src.toFun, map_add' := }, map_smul' := }
                      Instances For
                        @[simp]
                        theorem IsROrC.imLm_coe {K : Type u_1} [IsROrC K] :
                        IsROrC.imLm = IsROrC.im
                        noncomputable def IsROrC.imCLM {K : Type u_1} [IsROrC K] :

                        The imaginary part in an IsROrC field, as a continuous linear map.

                        Equations
                        Instances For
                          @[simp]
                          theorem IsROrC.imCLM_coe {K : Type u_1} [IsROrC K] :
                          IsROrC.imCLM = IsROrC.imLm
                          @[simp]
                          theorem IsROrC.imCLM_apply {K : Type u_1} [IsROrC K] :
                          IsROrC.imCLM = IsROrC.im
                          theorem IsROrC.continuous_im {K : Type u_1} [IsROrC K] :
                          Continuous IsROrC.im
                          def IsROrC.conjAe {K : Type u_1} [IsROrC K] :

                          Conjugate as an -algebra equivalence

                          Equations
                          • IsROrC.conjAe = let __src := starRingEnd K; { toEquiv := { toFun := __src.toFun, invFun := (starRingEnd K), left_inv := , right_inv := }, map_mul' := , map_add' := , commutes' := }
                          Instances For
                            @[simp]
                            theorem IsROrC.conjAe_coe {K : Type u_1} [IsROrC K] :
                            IsROrC.conjAe = (starRingEnd K)
                            noncomputable def IsROrC.conjLIE {K : Type u_1} [IsROrC K] :

                            Conjugate as a linear isometry

                            Equations
                            Instances For
                              @[simp]
                              theorem IsROrC.conjLIE_apply {K : Type u_1} [IsROrC K] :
                              IsROrC.conjLIE = (starRingEnd K)
                              noncomputable def IsROrC.conjCLE {K : Type u_1} [IsROrC K] :

                              Conjugate as a continuous linear equivalence

                              Equations
                              • IsROrC.conjCLE = { toLinearEquiv := IsROrC.conjLIE.toLinearEquiv, continuous_toFun := , continuous_invFun := }
                              Instances For
                                @[simp]
                                theorem IsROrC.conjCLE_coe {K : Type u_1} [IsROrC K] :
                                IsROrC.conjCLE.toLinearEquiv = AlgEquiv.toLinearEquiv IsROrC.conjAe
                                @[simp]
                                theorem IsROrC.conjCLE_apply {K : Type u_1} [IsROrC K] :
                                IsROrC.conjCLE = (starRingEnd K)
                                noncomputable def IsROrC.ofRealAm {K : Type u_1} [IsROrC K] :

                                The ℝ → K coercion, as a linear map

                                Equations
                                Instances For
                                  @[simp]
                                  theorem IsROrC.ofRealAm_coe {K : Type u_1} [IsROrC K] :
                                  IsROrC.ofRealAm = IsROrC.ofReal
                                  noncomputable def IsROrC.ofRealLI {K : Type u_1} [IsROrC K] :

                                  The ℝ → K coercion, as a linear isometry

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem IsROrC.ofRealLI_apply {K : Type u_1} [IsROrC K] :
                                    IsROrC.ofRealLI = IsROrC.ofReal
                                    noncomputable def IsROrC.ofRealCLM {K : Type u_1} [IsROrC K] :

                                    The ℝ → K coercion, as a continuous linear map

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem IsROrC.ofRealCLM_coe {K : Type u_1} [IsROrC K] :
                                      IsROrC.ofRealCLM = AlgHom.toLinearMap IsROrC.ofRealAm
                                      @[simp]
                                      theorem IsROrC.ofRealCLM_apply {K : Type u_1} [IsROrC K] :
                                      IsROrC.ofRealCLM = IsROrC.ofReal
                                      theorem IsROrC.continuous_ofReal {K : Type u_1} [IsROrC K] :
                                      Continuous IsROrC.ofReal
                                      theorem IsROrC.continuous_normSq {K : Type u_1} [IsROrC K] :
                                      Continuous IsROrC.normSq

                                      ℝ-dependent results #

                                      Here we gather results that depend on whether K is .

                                      theorem IsROrC.im_eq_zero {K : Type u_1} [IsROrC K] (h : IsROrC.I = 0) (z : K) :
                                      IsROrC.im z = 0
                                      @[simp]
                                      theorem IsROrC.realRingEquiv_symm_apply {K : Type u_1} [IsROrC K] (h : IsROrC.I = 0) :
                                      ∀ (a : ), (RingEquiv.symm (IsROrC.realRingEquiv h)) a = a
                                      @[simp]
                                      theorem IsROrC.realRingEquiv_apply {K : Type u_1} [IsROrC K] (h : IsROrC.I = 0) (a : K) :
                                      (IsROrC.realRingEquiv h) a = IsROrC.re a
                                      def IsROrC.realRingEquiv {K : Type u_1} [IsROrC K] (h : IsROrC.I = 0) :

                                      The natural isomorphism between 𝕜 satisfying IsROrC 𝕜 and when IsROrC.I = 0.

                                      Equations
                                      • IsROrC.realRingEquiv h = { toEquiv := { toFun := IsROrC.re, invFun := IsROrC.ofReal, left_inv := , right_inv := }, map_mul' := , map_add' := }
                                      Instances For
                                        @[simp]
                                        theorem IsROrC.realLinearIsometryEquiv_invFun {K : Type u_1} [IsROrC K] (h : IsROrC.I = 0) :
                                        ∀ (a : ), (IsROrC.realLinearIsometryEquiv h).invFun a = (IsROrC.realRingEquiv h).invFun a
                                        @[simp]
                                        theorem IsROrC.realLinearIsometryEquiv_apply {K : Type u_1} [IsROrC K] (h : IsROrC.I = 0) :
                                        @[simp]
                                        theorem IsROrC.realLinearIsometryEquiv_toFun {K : Type u_1} [IsROrC K] (h : IsROrC.I = 0) :
                                        noncomputable def IsROrC.realLinearIsometryEquiv {K : Type u_1} [IsROrC K] (h : IsROrC.I = 0) :

                                        The natural -linear isometry equivalence between 𝕜 satisfying IsROrC 𝕜 and when IsROrC.I = 0.

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