RCLike: a typeclass for ℝ or ℂ

This file defines the typeclass RCLike 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 RCLike field is done by registering RCLike.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/RCLike/Lemmas.lean.

class RCLike (K : semiOutParam (Type u_1)) extends DenselyNormedField , StarRing , NormedAlgebra , CompleteSpace : Type u_1

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

• norm : K → ℝ
• add : K → K → K
• add_assoc : ∀ (a b c : K), a + b + c = a + (b + c)
• zero : K
• zero_add : ∀ (a : K), 0 + a = a
• add_zero : ∀ (a : K), a + 0 = a
• nsmul : ℕ → K → K
• nsmul_zero : ∀ (x : K), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : K), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm : ∀ (a b : K), a + b = b + a
• mul : K → K → K
• left_distrib : ∀ (a b c : K), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : K), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : K), 0 * a = 0
• mul_zero : ∀ (a : K), a * 0 = 0
• mul_assoc : ∀ (a b c : K), a * b * c = a * (b * c)
• one : K
• one_mul : ∀ (a : K), 1 * a = a
• mul_one : ∀ (a : K), a * 1 = a
• natCast : ℕ → K
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → K → K
• npow_zero : ∀ (x : K), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : K), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : K → K
• sub : K → K → K
• sub_eq_add_neg : ∀ (a b : K), a - b = a + -b
• zsmul : ℤ → K → K
• zsmul_zero' : ∀ (a : K), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : K), -a + a = 0
• intCast : ℤ → K
• intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
• intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm : ∀ (a b : K), a * b = b * a
• inv : K → K
• div : K → K → K
• div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹
• zpow : ℤ → K → K
• zpow_zero' : ∀ (a : K), Field.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : K), Field.zpow (Int.ofNat n.succ) a = Field.zpow (Int.ofNat n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : K), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : K) (y : K), x ≠ y
• nnratCast : ℚ≥0 → K
• ratCast : ℚ → K
• mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → K → K
• nnqsmul_def : ∀ (q : ℚ≥0) (a : K), Field.nnqsmul q a = ↑q * a
• ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → K → K
• qsmul_def : ∀ (a : ℚ) (x : K), Field.qsmul a x = ↑a * x
• dist : K → K → ℝ
• dist_self : ∀ (x : K), dist x x = 0
• dist_comm : ∀ (x y : K), dist x y = dist y x
• dist_triangle : ∀ (x y z : K), dist x z ≤ dist x y + dist y z
• edist : K → K → ENNReal
• edist_dist : ∀ (x y : K), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace K
• uniformity_dist : uniformity K = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : K × K | dist p.1 p.2 < ε}
• toBornology : Bornology K
• cobounded_sets : (Bornology.cobounded K).sets = {s : Set K | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero : ∀ {x y : K}, dist x y = 0 → x = y
• dist_eq : ∀ (x y : K), dist x y = ‖x - y‖
• norm_mul' : ∀ (a b : K), ‖a * b‖ = ‖a‖ * ‖b‖
• lt_norm_lt : ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ (a : K), x < ‖a‖ ∧ ‖a‖ < y
• star : K → K
• star_involutive : Function.Involutive star
• star_mul : ∀ (r s : K), star (r * s) = star s * star r
• star_add : ∀ (r s : K), star (r + s) = star r + star s
• smul : ℝ → K → K
• toFun : ℝ → K
• map_one' : (↑↑Algebra.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : ℝ), (↑↑Algebra.toRingHom).toFun (x * y) = (↑↑Algebra.toRingHom).toFun x * (↑↑Algebra.toRingHom).toFun y
• map_zero' : (↑↑Algebra.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : ℝ), (↑↑Algebra.toRingHom).toFun (x + y) = (↑↑Algebra.toRingHom).toFun x + (↑↑Algebra.toRingHom).toFun y
• commutes' : ∀ (r : ℝ) (x : K), Algebra.toRingHom r * x = x * Algebra.toRingHom r
• smul_def' : ∀ (r : ℝ) (x : K), r • x = Algebra.toRingHom r * x
• norm_smul_le : ∀ (r : ℝ) (x : K), ‖r • x‖ ≤ ‖r‖ * ‖x‖
• complete : ∀ {f : Filter K}, Cauchy f → ∃ (x : K), f ≤ nhds x
• re : K →+ ℝ
• im : K →+ ℝ
• I : K

  Imaginary unit in K. Meant to be set to 0 for K = ℝ.

• I_re_ax : RCLike.re RCLike.I = 0
• I_mul_I_ax : RCLike.I = 0 ∨ RCLike.I * RCLike.I = -1
• re_add_im_ax : ∀ (z : K), (algebraMap ℝ K) (RCLike.re z) + (algebraMap ℝ K) (RCLike.im z) * RCLike.I = z
• ofReal_re_ax : ∀ (r : ℝ), RCLike.re ((algebraMap ℝ K) r) = r
• ofReal_im_ax : ∀ (r : ℝ), RCLike.im ((algebraMap ℝ K) r) = 0
• mul_re_ax : ∀ (z w : K), RCLike.re (z * w) = RCLike.re z * RCLike.re w - RCLike.im z * RCLike.im w
• mul_im_ax : ∀ (z w : K), RCLike.im (z * w) = RCLike.re z * RCLike.im w + RCLike.im z * RCLike.re w
• conj_re_ax : ∀ (z : K), RCLike.re ((starRingEnd K) z) = RCLike.re z
• conj_im_ax : ∀ (z : K), RCLike.im ((starRingEnd K) z) = -RCLike.im z
• conj_I_ax : (starRingEnd K) RCLike.I = -RCLike.I
• norm_sq_eq_def_ax : ∀ (z : K), ‖z‖ ^ 2 = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z
• mul_im_I_ax : ∀ (z : K), RCLike.im z * RCLike.im RCLike.I = RCLike.im z
• toPartialOrder : PartialOrder K

  only an instance in the ComplexOrder locale

• le_iff_re_im : ∀ {z w : K}, z ≤ w ↔ RCLike.re z ≤ RCLike.re w ∧ RCLike.im z = RCLike.im w
• toDecidableEq : DecidableEq K

theorem RCLike.I_re_ax {K : semiOutParam (Type u_1)} [self : RCLike K] : RCLike.re RCLike.I = 0

theorem RCLike.I_mul_I_ax {K : semiOutParam (Type u_1)} [self : RCLike K] : RCLike.I = 0 ∨ RCLike.I * RCLike.I = -1

theorem RCLike.re_add_im_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K) : (algebraMap ℝ K) (RCLike.re z) + (algebraMap ℝ K) (RCLike.im z) * RCLike.I = z

theorem RCLike.ofReal_re_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (r : ℝ) : RCLike.re ((algebraMap ℝ K) r) = r

theorem RCLike.ofReal_im_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (r : ℝ) : RCLike.im ((algebraMap ℝ K) r) = 0

theorem RCLike.mul_re_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K) (w : K) : RCLike.re (z * w) = RCLike.re z * RCLike.re w - RCLike.im z * RCLike.im w

theorem RCLike.mul_im_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K) (w : K) : RCLike.im (z * w) = RCLike.re z * RCLike.im w + RCLike.im z * RCLike.re w

theorem RCLike.conj_re_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K) : RCLike.re ((starRingEnd K) z) = RCLike.re z

theorem RCLike.conj_im_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K) : RCLike.im ((starRingEnd K) z) = -RCLike.im z

theorem RCLike.conj_I_ax {K : semiOutParam (Type u_1)} [self : RCLike K] : (starRingEnd K) RCLike.I = -RCLike.I

theorem RCLike.norm_sq_eq_def_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K) : ‖z‖ ^ 2 = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z

theorem RCLike.mul_im_I_ax {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K) : RCLike.im z * RCLike.im RCLike.I = RCLike.im z

theorem RCLike.le_iff_re_im {K : semiOutParam (Type u_1)} [self : RCLike K] {z : K} {w : K} : z ≤ w ↔ RCLike.re z ≤ RCLike.re w ∧ RCLike.im z = RCLike.im w

@[reducible, inline]

abbrev RCLike.ofReal {K : Type u_1} [RCLike K] : ℝ → K

Coercion from ℝ to an RCLike field.

Equations

• RCLike.ofReal = Algebra.cast

@[instance 900]

noncomputable instance RCLike.algebraMapCoe {K : Type u_1} [RCLike K] : CoeTC ℝ K

Equations

• RCLike.algebraMapCoe = { coe := RCLike.ofReal }

theorem RCLike.ofReal_alg {K : Type u_1} [RCLike K] (x : ℝ) : ↑x = x • 1

theorem RCLike.real_smul_eq_coe_mul {K : Type u_1} [RCLike K] (r : ℝ) (z : K) : r • z = ↑r * z

theorem RCLike.real_smul_eq_coe_smul {K : Type u_1} {E : Type u_2} [RCLike K] [AddCommGroup E] [Module K E] [Module ℝ E] [IsScalarTower ℝ K E] (r : ℝ) (x : E) : r • x = ↑r • x

theorem RCLike.algebraMap_eq_ofReal {K : Type u_1} [RCLike K] : ⇑(algebraMap ℝ K) = RCLike.ofReal

@[simp]

theorem RCLike.re_add_im {K : Type u_1} [RCLike K] (z : K) : ↑(RCLike.re z) + ↑(RCLike.im z) * RCLike.I = z

@[simp]

theorem RCLike.ofReal_re {K : Type u_1} [RCLike K] (r : ℝ) : RCLike.re ↑r = r

@[simp]

theorem RCLike.ofReal_im {K : Type u_1} [RCLike K] (r : ℝ) : RCLike.im ↑r = 0

@[simp]

theorem RCLike.mul_re {K : Type u_1} [RCLike K] (z : K) (w : K) : RCLike.re (z * w) = RCLike.re z * RCLike.re w - RCLike.im z * RCLike.im w

@[simp]

theorem RCLike.mul_im {K : Type u_1} [RCLike K] (z : K) (w : K) : RCLike.im (z * w) = RCLike.re z * RCLike.im w + RCLike.im z * RCLike.re w

theorem RCLike.ext_iff {K : Type u_1} [RCLike K] {z : K} {w : K} : z = w ↔ RCLike.re z = RCLike.re w ∧ RCLike.im z = RCLike.im w

theorem RCLike.ext {K : Type u_1} [RCLike K] {z : K} {w : K} (hre : RCLike.re z = RCLike.re w) (him : RCLike.im z = RCLike.im w) : z = w

theorem RCLike.ofReal_zero {K : Type u_1} [RCLike K] : ↑0 = 0

theorem RCLike.zero_re' {K : Type u_1} [RCLike K] : RCLike.re 0 = 0

theorem RCLike.ofReal_one {K : Type u_1} [RCLike K] : ↑1 = 1

@[simp]

theorem RCLike.one_re {K : Type u_1} [RCLike K] : RCLike.re 1 = 1

@[simp]

theorem RCLike.one_im {K : Type u_1} [RCLike K] : RCLike.im 1 = 0

theorem RCLike.ofReal_injective {K : Type u_1} [RCLike K] : Function.Injective RCLike.ofReal

theorem RCLike.ofReal_inj {K : Type u_1} [RCLike K] {z : ℝ} {w : ℝ} : ↑z = ↑w ↔ z = w

theorem RCLike.ofReal_eq_zero {K : Type u_1} [RCLike K] {x : ℝ} : ↑x = 0 ↔ x = 0

theorem RCLike.ofReal_ne_zero {K : Type u_1} [RCLike K] {x : ℝ} : ↑x ≠ 0 ↔ x ≠ 0

theorem RCLike.ofReal_add {K : Type u_1} [RCLike K] (r : ℝ) (s : ℝ) : ↑(r + s) = ↑r + ↑s

theorem RCLike.ofReal_neg {K : Type u_1} [RCLike K] (r : ℝ) : ↑(-r) = -↑r

theorem RCLike.ofReal_sub {K : Type u_1} [RCLike K] (r : ℝ) (s : ℝ) : ↑(r - s) = ↑r - ↑s

theorem RCLike.ofReal_sum {K : Type u_1} [RCLike K] {α : Type u_3} (s : Finset α) (f : α → ℝ) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

@[simp]

theorem RCLike.ofReal_finsupp_sum {K : Type u_1} [RCLike K] {α : Type u_3} {M : Type u_4} [Zero M] (f : α →₀ M) (g : α → M → ℝ) : ↑(f.sum fun (a : α) (b : M) => g a b) = f.sum fun (a : α) (b : M) => ↑(g a b)

theorem RCLike.ofReal_mul {K : Type u_1} [RCLike K] (r : ℝ) (s : ℝ) : ↑(r * s) = ↑r * ↑s

theorem RCLike.ofReal_pow {K : Type u_1} [RCLike K] (r : ℝ) (n : ℕ) : ↑(r ^ n) = ↑r ^ n

theorem RCLike.ofReal_prod {K : Type u_1} [RCLike K] {α : Type u_3} (s : Finset α) (f : α → ℝ) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

@[simp]

theorem RCLike.ofReal_finsupp_prod {K : Type u_1} [RCLike K] {α : Type u_3} {M : Type u_4} [Zero M] (f : α →₀ M) (g : α → M → ℝ) : ↑(f.prod fun (a : α) (b : M) => g a b) = f.prod fun (a : α) (b : M) => ↑(g a b)

@[simp]

theorem RCLike.real_smul_ofReal {K : Type u_1} [RCLike K] (r : ℝ) (x : ℝ) : r • ↑x = ↑r * ↑x

theorem RCLike.re_ofReal_mul {K : Type u_1} [RCLike K] (r : ℝ) (z : K) : RCLike.re (↑r * z) = r * RCLike.re z

theorem RCLike.im_ofReal_mul {K : Type u_1} [RCLike K] (r : ℝ) (z : K) : RCLike.im (↑r * z) = r * RCLike.im z

theorem RCLike.smul_re {K : Type u_1} [RCLike K] (r : ℝ) (z : K) : RCLike.re (r • z) = r * RCLike.re z

theorem RCLike.smul_im {K : Type u_1} [RCLike K] (r : ℝ) (z : K) : RCLike.im (r • z) = r * RCLike.im z

theorem RCLike.norm_ofReal {K : Type u_1} [RCLike K] (r : ℝ) : ‖↑r‖ = |r|

Characteristic zero

@[instance 100]

instance RCLike.charZero_rclike {K : Type u_1} [RCLike K] : CharZero K

ℝ and ℂ are both of characteristic zero.

Equations

• ⋯ = ⋯

theorem RCLike.ofReal_expect {K : Type u_1} [RCLike K] {α : Type u_3} (s : Finset α) (f : α → ℝ) : ↑(s.expect fun (i : α) => f i) = s.expect fun (i : α) => ↑(f i)

The imaginary unit, I

@[simp]

theorem RCLike.I_re {K : Type u_1} [RCLike K] : RCLike.re RCLike.I = 0

The imaginary unit.

@[simp]

theorem RCLike.I_im {K : Type u_1} [RCLike K] (z : K) : RCLike.im z * RCLike.im RCLike.I = RCLike.im z

@[simp]

theorem RCLike.I_im' {K : Type u_1} [RCLike K] (z : K) : RCLike.im RCLike.I * RCLike.im z = RCLike.im z

theorem RCLike.I_mul_re {K : Type u_1} [RCLike K] (z : K) : RCLike.re (RCLike.I * z) = -RCLike.im z

theorem RCLike.I_mul_I {K : Type u_1} [RCLike K] : RCLike.I = 0 ∨ RCLike.I * RCLike.I = -1

theorem RCLike.I_eq_zero_or_im_I_eq_one {K : Type u_1} [RCLike K] : RCLike.I = 0 ∨ RCLike.im RCLike.I = 1

@[simp]

theorem RCLike.conj_re {K : Type u_1} [RCLike K] (z : K) : RCLike.re ((starRingEnd K) z) = RCLike.re z

@[simp]

theorem RCLike.conj_im {K : Type u_1} [RCLike K] (z : K) : RCLike.im ((starRingEnd K) z) = -RCLike.im z

@[simp]

theorem RCLike.conj_I {K : Type u_1} [RCLike K] : (starRingEnd K) RCLike.I = -RCLike.I

@[simp]

theorem RCLike.conj_ofReal {K : Type u_1} [RCLike K] (r : ℝ) : (starRingEnd K) ↑r = ↑r

theorem RCLike.conj_nat_cast {K : Type u_1} [RCLike K] (n : ℕ) : (starRingEnd K) ↑n = ↑n

theorem RCLike.conj_ofNat {K : Type u_1} [RCLike K] (n : ℕ) [n.AtLeastTwo] : (starRingEnd K) (OfNat.ofNat n) = OfNat.ofNat n

theorem RCLike.conj_neg_I {K : Type u_1} [RCLike K] : (starRingEnd K) (-RCLike.I) = RCLike.I

theorem RCLike.conj_eq_re_sub_im {K : Type u_1} [RCLike K] (z : K) : (starRingEnd K) z = ↑(RCLike.re z) - ↑(RCLike.im z) * RCLike.I

theorem RCLike.sub_conj {K : Type u_1} [RCLike K] (z : K) : z - (starRingEnd K) z = 2 * ↑(RCLike.im z) * RCLike.I

theorem RCLike.conj_smul {K : Type u_1} [RCLike K] (r : ℝ) (z : K) : (starRingEnd K) (r • z) = r • (starRingEnd K) z

theorem RCLike.add_conj {K : Type u_1} [RCLike K] (z : K) : z + (starRingEnd K) z = 2 * ↑(RCLike.re z)

theorem RCLike.re_eq_add_conj {K : Type u_1} [RCLike K] (z : K) : ↑(RCLike.re z) = (z + (starRingEnd K) z) / 2

theorem RCLike.im_eq_conj_sub {K : Type u_1} [RCLike K] (z : K) : ↑(RCLike.im z) = RCLike.I * ((starRingEnd K) z - z) / 2

theorem RCLike.is_real_TFAE {K : Type u_1} [RCLike K] (z : K) : [(starRingEnd K) z = z, ∃ (r : ℝ), ↑r = z, ↑(RCLike.re z) = z, RCLike.im z = 0].TFAE

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

theorem RCLike.conj_eq_iff_real {K : Type u_1} [RCLike K] {z : K} : (starRingEnd K) z = z ↔ ∃ (r : ℝ), z = ↑r

theorem RCLike.conj_eq_iff_re {K : Type u_1} [RCLike K] {z : K} : (starRingEnd K) z = z ↔ ↑(RCLike.re z) = z

theorem RCLike.conj_eq_iff_im {K : Type u_1} [RCLike K] {z : K} : (starRingEnd K) z = z ↔ RCLike.im z = 0

@[simp]

theorem RCLike.star_def {K : Type u_1} [RCLike K] : star = ⇑(starRingEnd K)

@[reducible, inline]

abbrev RCLike.conjToRingEquiv (K : Type u_1) [RCLike K] : K ≃+* Kᵐᵒᵖ

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

Equations

• RCLike.conjToRingEquiv K = starRingEquiv

def RCLike.normSq {K : Type u_1} [RCLike K] : K →*₀ ℝ

The norm squared function.

Equations

• RCLike.normSq = { toFun := fun (z : K) => RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem RCLike.normSq_apply {K : Type u_1} [RCLike K] (z : K) : RCLike.normSq z = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z

theorem RCLike.norm_sq_eq_def {K : Type u_1} [RCLike K] {z : K} : ‖z‖ ^ 2 = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z

theorem RCLike.normSq_eq_def' {K : Type u_1} [RCLike K] (z : K) : RCLike.normSq z = ‖z‖ ^ 2

theorem RCLike.normSq_zero {K : Type u_1} [RCLike K] : RCLike.normSq 0 = 0

theorem RCLike.normSq_one {K : Type u_1} [RCLike K] : RCLike.normSq 1 = 1

theorem RCLike.normSq_nonneg {K : Type u_1} [RCLike K] (z : K) : 0 ≤ RCLike.normSq z

theorem RCLike.normSq_eq_zero {K : Type u_1} [RCLike K] {z : K} : RCLike.normSq z = 0 ↔ z = 0

@[simp]

theorem RCLike.normSq_pos {K : Type u_1} [RCLike K] {z : K} : 0 < RCLike.normSq z ↔ z ≠ 0

@[simp]

theorem RCLike.normSq_neg {K : Type u_1} [RCLike K] (z : K) : RCLike.normSq (-z) = RCLike.normSq z

@[simp]

theorem RCLike.normSq_conj {K : Type u_1} [RCLike K] (z : K) : RCLike.normSq ((starRingEnd K) z) = RCLike.normSq z

theorem RCLike.normSq_mul {K : Type u_1} [RCLike K] (z : K) (w : K) : RCLike.normSq (z * w) = RCLike.normSq z * RCLike.normSq w

theorem RCLike.normSq_add {K : Type u_1} [RCLike K] (z : K) (w : K) : RCLike.normSq (z + w) = RCLike.normSq z + RCLike.normSq w + 2 * RCLike.re (z * (starRingEnd K) w)

theorem RCLike.re_sq_le_normSq {K : Type u_1} [RCLike K] (z : K) : RCLike.re z * RCLike.re z ≤ RCLike.normSq z

theorem RCLike.im_sq_le_normSq {K : Type u_1} [RCLike K] (z : K) : RCLike.im z * RCLike.im z ≤ RCLike.normSq z

theorem RCLike.mul_conj {K : Type u_1} [RCLike K] (z : K) : z * (starRingEnd K) z = ↑‖z‖ ^ 2

theorem RCLike.conj_mul {K : Type u_1} [RCLike K] (z : K) : (starRingEnd K) z * z = ↑‖z‖ ^ 2

theorem RCLike.inv_eq_conj {K : Type u_1} [RCLike K] {z : K} (hz : ‖z‖ = 1) : z⁻¹ = (starRingEnd K) z

theorem RCLike.normSq_sub {K : Type u_1} [RCLike K] (z : K) (w : K) : RCLike.normSq (z - w) = RCLike.normSq z + RCLike.normSq w - 2 * RCLike.re (z * (starRingEnd K) w)

theorem RCLike.sqrt_normSq_eq_norm {K : Type u_1} [RCLike K] {z : K} : √(RCLike.normSq z) = ‖z‖

Inversion

theorem RCLike.ofReal_inv {K : Type u_1} [RCLike K] (r : ℝ) : ↑r⁻¹ = (↑r)⁻¹

theorem RCLike.inv_def {K : Type u_1} [RCLike K] (z : K) : z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

@[simp]

theorem RCLike.inv_re {K : Type u_1} [RCLike K] (z : K) : RCLike.re z⁻¹ = RCLike.re z / RCLike.normSq z

@[simp]

theorem RCLike.inv_im {K : Type u_1} [RCLike K] (z : K) : RCLike.im z⁻¹ = -RCLike.im z / RCLike.normSq z

theorem RCLike.div_re {K : Type u_1} [RCLike K] (z : K) (w : K) : RCLike.re (z / w) = RCLike.re z * RCLike.re w / RCLike.normSq w + RCLike.im z * RCLike.im w / RCLike.normSq w

theorem RCLike.div_im {K : Type u_1} [RCLike K] (z : K) (w : K) : RCLike.im (z / w) = RCLike.im z * RCLike.re w / RCLike.normSq w - RCLike.re z * RCLike.im w / RCLike.normSq w

theorem RCLike.conj_inv {K : Type u_1} [RCLike K] (x : K) : (starRingEnd K) x⁻¹ = ((starRingEnd K) x)⁻¹

theorem RCLike.conj_div {K : Type u_1} [RCLike K] (x : K) (y : K) : (starRingEnd K) (x / y) = (starRingEnd K) x / (starRingEnd K) y

theorem RCLike.exists_norm_eq_mul_self {K : Type u_1} [RCLike K] (x : K) : ∃ (c : K), ‖c‖ = 1 ∧ ↑‖x‖ = c * x

theorem RCLike.exists_norm_mul_eq_self {K : Type u_1} [RCLike K] (x : K) : ∃ (c : K), ‖c‖ = 1 ∧ c * ↑‖x‖ = x

theorem RCLike.ofReal_div {K : Type u_1} [RCLike K] (r : ℝ) (s : ℝ) : ↑(r / s) = ↑r / ↑s

theorem RCLike.div_re_ofReal {K : Type u_1} [RCLike K] {z : K} {r : ℝ} : RCLike.re (z / ↑r) = RCLike.re z / r

theorem RCLike.ofReal_zpow {K : Type u_1} [RCLike K] (r : ℝ) (n : ℤ) : ↑(r ^ n) = ↑r ^ n

theorem RCLike.I_mul_I_of_nonzero {K : Type u_1} [RCLike K] : RCLike.I ≠ 0 → RCLike.I * RCLike.I = -1

@[simp]

theorem RCLike.inv_I {K : Type u_1} [RCLike K] : RCLike.I⁻¹ = -RCLike.I

@[simp]

theorem RCLike.div_I {K : Type u_1} [RCLike K] (z : K) : z / RCLike.I = -(z * RCLike.I)

theorem RCLike.normSq_inv {K : Type u_1} [RCLike K] (z : K) : RCLike.normSq z⁻¹ = (RCLike.normSq z)⁻¹

theorem RCLike.normSq_div {K : Type u_1} [RCLike K] (z : K) (w : K) : RCLike.normSq (z / w) = RCLike.normSq z / RCLike.normSq w

@[simp]

theorem RCLike.norm_conj {K : Type u_1} [RCLike K] (z : K) : ‖(starRingEnd K) z‖ = ‖z‖

@[simp]

theorem RCLike.nnnorm_conj {K : Type u_1} [RCLike K] (z : K) : ‖(starRingEnd K) z‖₊ = ‖z‖₊

@[instance 100]

instance RCLike.instCStarRing {K : Type u_1} [RCLike K] : CStarRing K

Equations

• ⋯ = ⋯

Cast lemmas

theorem RCLike.ofReal_natCast {K : Type u_1} [RCLike K] (n : ℕ) : ↑↑n = ↑n

theorem RCLike.ofReal_nnratCast {K : Type u_1} [RCLike K] (q : ℚ≥0) : ↑↑q = ↑q

@[simp]

theorem RCLike.natCast_re {K : Type u_1} [RCLike K] (n : ℕ) : RCLike.re ↑n = ↑n

@[simp]

theorem RCLike.natCast_im {K : Type u_1} [RCLike K] (n : ℕ) : RCLike.im ↑n = 0

@[simp]

theorem RCLike.ofNat_re {K : Type u_1} [RCLike K] (n : ℕ) [n.AtLeastTwo] : RCLike.re (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem RCLike.ofNat_im {K : Type u_1} [RCLike K] (n : ℕ) [n.AtLeastTwo] : RCLike.im (OfNat.ofNat n) = 0

theorem RCLike.ofReal_ofNat {K : Type u_1} [RCLike K] (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n

theorem RCLike.ofNat_mul_re {K : Type u_1} [RCLike K] (n : ℕ) [n.AtLeastTwo] (z : K) : RCLike.re (OfNat.ofNat n * z) = OfNat.ofNat n * RCLike.re z

theorem RCLike.ofNat_mul_im {K : Type u_1} [RCLike K] (n : ℕ) [n.AtLeastTwo] (z : K) : RCLike.im (OfNat.ofNat n * z) = OfNat.ofNat n * RCLike.im z

theorem RCLike.ofReal_intCast {K : Type u_1} [RCLike K] (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem RCLike.intCast_re {K : Type u_1} [RCLike K] (n : ℤ) : RCLike.re ↑n = ↑n

@[simp]

theorem RCLike.intCast_im {K : Type u_1} [RCLike K] (n : ℤ) : RCLike.im ↑n = 0

theorem RCLike.ofReal_ratCast {K : Type u_1} [RCLike K] (n : ℚ) : ↑↑n = ↑n

@[simp]

theorem RCLike.ratCast_re {K : Type u_1} [RCLike K] (q : ℚ) : RCLike.re ↑q = ↑q

@[simp]

theorem RCLike.ratCast_im {K : Type u_1} [RCLike K] (q : ℚ) : RCLike.im ↑q = 0

Norm

theorem RCLike.norm_of_nonneg {K : Type u_1} [RCLike K] {r : ℝ} (h : 0 ≤ r) : ‖↑r‖ = r

@[simp]

theorem RCLike.norm_natCast {K : Type u_1} [RCLike K] (n : ℕ) : ‖↑n‖ = ↑n

@[simp]

theorem RCLike.nnnorm_natCast {K : Type u_1} [RCLike K] (n : ℕ) : ‖↑n‖₊ = ↑n

@[simp]

theorem RCLike.norm_ofNat {K : Type u_1} [RCLike K] (n : ℕ) [n.AtLeastTwo] : ‖OfNat.ofNat n‖ = OfNat.ofNat n

@[simp]

theorem RCLike.nnnorm_ofNat {K : Type u_1} [RCLike K] (n : ℕ) [n.AtLeastTwo] : ‖OfNat.ofNat n‖₊ = OfNat.ofNat n

theorem RCLike.norm_two {K : Type u_1} [RCLike K] : ‖2‖ = 2

theorem RCLike.nnnorm_two {K : Type u_1} [RCLike K] : ‖2‖₊ = 2

@[simp]

theorem RCLike.norm_nnratCast {K : Type u_1} [RCLike K] (q : ℚ≥0) : ‖↑q‖ = ↑q

@[simp]

theorem RCLike.nnnorm_nnratCast {K : Type u_1} [RCLike K] (q : ℚ≥0) : ‖↑q‖₊ = ↑q

theorem RCLike.norm_nsmul (K : Type u_1) {E : Type u_2} [RCLike K] [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) : ‖n • x‖ = n • ‖x‖

theorem RCLike.nnnorm_nsmul (K : Type u_1) {E : Type u_2} [RCLike K] [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) : ‖n • x‖₊ = n • ‖x‖₊

theorem RCLike.norm_nnqsmul (K : Type u_1) {E : Type u_2} [RCLike K] [NormedField E] [CharZero E] [NormedSpace K E] (q : ℚ≥0) (x : E) : ‖q • x‖ = q • ‖x‖

theorem RCLike.nnnorm_nnqsmul (K : Type u_1) {E : Type u_2} [RCLike K] [NormedField E] [CharZero E] [NormedSpace K E] (q : ℚ≥0) (x : E) : ‖q • x‖₊ = q • ‖x‖₊

theorem RCLike.norm_expect_le {K : Type u_1} {E : Type u_2} [RCLike K] [NormedField E] [CharZero E] [NormedSpace K E] {ι : Type u_3} {s : Finset ι} {f : ι → E} : ‖s.expect fun (i : ι) => f i‖ ≤ s.expect fun (i : ι) => ‖f i‖

theorem RCLike.mul_self_norm {K : Type u_1} [RCLike K] (z : K) : ‖z‖ * ‖z‖ = RCLike.normSq z

theorem RCLike.abs_re_le_norm {K : Type u_1} [RCLike K] (z : K) : |RCLike.re z| ≤ ‖z‖

theorem RCLike.abs_im_le_norm {K : Type u_1} [RCLike K] (z : K) : |RCLike.im z| ≤ ‖z‖

theorem RCLike.norm_re_le_norm {K : Type u_1} [RCLike K] (z : K) : ‖RCLike.re z‖ ≤ ‖z‖

theorem RCLike.norm_im_le_norm {K : Type u_1} [RCLike K] (z : K) : ‖RCLike.im z‖ ≤ ‖z‖

theorem RCLike.re_le_norm {K : Type u_1} [RCLike K] (z : K) : RCLike.re z ≤ ‖z‖

theorem RCLike.im_le_norm {K : Type u_1} [RCLike K] (z : K) : RCLike.im z ≤ ‖z‖

theorem RCLike.im_eq_zero_of_le {K : Type u_1} [RCLike K] {a : K} (h : ‖a‖ ≤ RCLike.re a) : RCLike.im a = 0

theorem RCLike.re_eq_self_of_le {K : Type u_1} [RCLike K] {a : K} (h : ‖a‖ ≤ RCLike.re a) : ↑(RCLike.re a) = a

theorem RCLike.abs_re_div_norm_le_one {K : Type u_1} [RCLike K] (z : K) : |RCLike.re z / ‖z‖| ≤ 1

theorem RCLike.abs_im_div_norm_le_one {K : Type u_1} [RCLike K] (z : K) : |RCLike.im z / ‖z‖| ≤ 1

theorem RCLike.norm_I_of_ne_zero {K : Type u_1} [RCLike K] (hI : RCLike.I ≠ 0) : ‖RCLike.I‖ = 1

theorem RCLike.re_eq_norm_of_mul_conj {K : Type u_1} [RCLike K] (x : K) : RCLike.re (x * (starRingEnd K) x) = ‖x * (starRingEnd K) x‖

theorem RCLike.norm_sq_re_add_conj {K : Type u_1} [RCLike K] (x : K) : ‖x + (starRingEnd K) x‖ ^ 2 = RCLike.re (x + (starRingEnd K) x) ^ 2

theorem RCLike.norm_sq_re_conj_add {K : Type u_1} [RCLike K] (x : K) : ‖(starRingEnd K) x + x‖ ^ 2 = RCLike.re ((starRingEnd K) x + x) ^ 2

Cauchy sequences

theorem RCLike.isCauSeq_re {K : Type u_1} [RCLike K] (f : CauSeq K norm) : IsCauSeq abs fun (n : ℕ) => RCLike.re (↑f n)

theorem RCLike.isCauSeq_im {K : Type u_1} [RCLike K] (f : CauSeq K norm) : IsCauSeq abs fun (n : ℕ) => RCLike.im (↑f n)

noncomputable def RCLike.cauSeqRe {K : Type u_1} [RCLike K] (f : CauSeq K norm) : CauSeq ℝ abs

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

Equations

• RCLike.cauSeqRe f = ⟨fun (n : ℕ) => RCLike.re (↑f n), ⋯⟩

noncomputable def RCLike.cauSeqIm {K : Type u_1} [RCLike K] (f : CauSeq K norm) : CauSeq ℝ abs

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

Equations

• RCLike.cauSeqIm f = ⟨fun (n : ℕ) => RCLike.im (↑f n), ⋯⟩

theorem RCLike.isCauSeq_norm {K : Type u_1} [RCLike K] {f : ℕ → K} (hf : IsCauSeq norm f) : IsCauSeq abs (norm ∘ f)

noncomputable instance Real.instRCLike : RCLike ℝ

Equations

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

theorem RCLike.lt_iff_re_im {K : Type u_1} [RCLike K] {z : K} {w : K} : z < w ↔ RCLike.re z < RCLike.re w ∧ RCLike.im z = RCLike.im w

theorem RCLike.nonneg_iff {K : Type u_1} [RCLike K] {z : K} : 0 ≤ z ↔ 0 ≤ RCLike.re z ∧ RCLike.im z = 0

theorem RCLike.pos_iff {K : Type u_1} [RCLike K] {z : K} : 0 < z ↔ 0 < RCLike.re z ∧ RCLike.im z = 0

theorem RCLike.nonpos_iff {K : Type u_1} [RCLike K] {z : K} : z ≤ 0 ↔ RCLike.re z ≤ 0 ∧ RCLike.im z = 0

theorem RCLike.neg_iff {K : Type u_1} [RCLike K] {z : K} : z < 0 ↔ RCLike.re z < 0 ∧ RCLike.im z = 0

theorem RCLike.nonneg_iff_exists_ofReal {K : Type u_1} [RCLike K] {z : K} : 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z

theorem RCLike.pos_iff_exists_ofReal {K : Type u_1} [RCLike K] {z : K} : 0 < z ↔ ∃ x > 0, ↑x = z

theorem RCLike.nonpos_iff_exists_ofReal {K : Type u_1} [RCLike K] {z : K} : z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z

theorem RCLike.neg_iff_exists_ofReal {K : Type u_1} [RCLike K] {z : K} : z < 0 ↔ ∃ x < 0, ↑x = z

@[simp]

theorem RCLike.ofReal_le_ofReal {K : Type u_1} [RCLike K] {x : ℝ} {y : ℝ} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem RCLike.ofReal_lt_ofReal {K : Type u_1} [RCLike K] {x : ℝ} {y : ℝ} : ↑x < ↑y ↔ x < y

@[simp]

theorem RCLike.ofReal_nonneg {K : Type u_1} [RCLike K] {x : ℝ} : 0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem RCLike.ofReal_nonpos {K : Type u_1} [RCLike K] {x : ℝ} : ↑x ≤ 0 ↔ x ≤ 0

@[simp]

theorem RCLike.ofReal_pos {K : Type u_1} [RCLike K] {x : ℝ} : 0 < ↑x ↔ 0 < x

@[simp]

theorem RCLike.ofReal_lt_zero {K : Type u_1} [RCLike K] {x : ℝ} : ↑x < 0 ↔ x < 0

theorem RCLike.inv_pos_of_pos {K : Type u_1} [RCLike K] {z : K} (hz : 0 < z) : 0 < z⁻¹

theorem RCLike.inv_pos {K : Type u_1} [RCLike K] {z : K} : 0 < z⁻¹ ↔ 0 < z

theorem RCLike.toStarOrderedRing {K : Type u_1} [RCLike K] : StarOrderedRing K

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.

def RCLike.toStrictOrderedCommRing {K : Type u_1} [RCLike K] : StrictOrderedCommRing K

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

• RCLike.toStrictOrderedCommRing = StrictOrderedCommRing.mk ⋯

theorem RCLike.toOrderedSMul {K : Type u_1} [RCLike K] : OrderedSMul ℝ K

theorem StarModule.instOrderedSMul {K : Type u_1} [RCLike K] {A : Type u_3} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module K A] [StarModule K A] [IsScalarTower K A A] [SMulCommClass K A A] : OrderedSMul K A

A star algebra over K has a scalar multiplication that respects the order.

instance RCLike.instOrderedSMulRealOfStarModuleOfIsScalarTowerOfSMulCommClass {A : Type u_3} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module ℝ A] [StarModule ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] : OrderedSMul ℝ A

Equations

• ⋯ = ⋯

@[simp]

theorem RCLike.re_to_real {x : ℝ} : RCLike.re x = x

@[simp]

theorem RCLike.im_to_real {x : ℝ} : RCLike.im x = 0

theorem RCLike.conj_to_real {x : ℝ} : (starRingEnd ℝ) x = x

@[simp]

theorem RCLike.I_to_real : RCLike.I = 0

@[simp]

theorem RCLike.normSq_to_real {x : ℝ} : RCLike.normSq x = x * x

@[simp]

theorem RCLike.ofReal_real_eq_id : RCLike.ofReal = id

def RCLike.reLm {K : Type u_1} [RCLike K] : K →ₗ[ℝ] ℝ

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

Equations

• RCLike.reLm = { toFun := (↑RCLike.re).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RCLike.reLm_coe {K : Type u_1} [RCLike K] : ⇑RCLike.reLm = ⇑RCLike.re

noncomputable def RCLike.reCLM {K : Type u_1} [RCLike K] : K →L[ℝ] ℝ

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

Equations

• RCLike.reCLM = RCLike.reLm.mkContinuous 1 ⋯

@[simp]

theorem RCLike.reCLM_coe {K : Type u_1} [RCLike K] : ↑RCLike.reCLM = RCLike.reLm

@[simp]

theorem RCLike.reCLM_apply {K : Type u_1} [RCLike K] : ⇑RCLike.reCLM = ⇑RCLike.re

theorem RCLike.continuous_re {K : Type u_1} [RCLike K] : Continuous ⇑RCLike.re

def RCLike.imLm {K : Type u_1} [RCLike K] : K →ₗ[ℝ] ℝ

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

Equations

• RCLike.imLm = { toFun := (↑RCLike.im).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RCLike.imLm_coe {K : Type u_1} [RCLike K] : ⇑RCLike.imLm = ⇑RCLike.im

noncomputable def RCLike.imCLM {K : Type u_1} [RCLike K] : K →L[ℝ] ℝ

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

Equations

• RCLike.imCLM = RCLike.imLm.mkContinuous 1 ⋯

@[simp]

theorem RCLike.imCLM_coe {K : Type u_1} [RCLike K] : ↑RCLike.imCLM = RCLike.imLm

@[simp]

theorem RCLike.imCLM_apply {K : Type u_1} [RCLike K] : ⇑RCLike.imCLM = ⇑RCLike.im

theorem RCLike.continuous_im {K : Type u_1} [RCLike K] : Continuous ⇑RCLike.im

def RCLike.conjAe {K : Type u_1} [RCLike K] : K ≃ₐ[ℝ] K

Conjugate as an ℝ-algebra equivalence

Equations

• RCLike.conjAe = { toFun := (↑↑(starRingEnd K)).toFun, invFun := ⇑(starRingEnd K), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem RCLike.conjAe_coe {K : Type u_1} [RCLike K] : ⇑RCLike.conjAe = ⇑(starRingEnd K)

noncomputable def RCLike.conjLIE {K : Type u_1} [RCLike K] : K ≃ₗᵢ[ℝ] K

Conjugate as a linear isometry

Equations

• RCLike.conjLIE = { toLinearEquiv := RCLike.conjAe.toLinearEquiv, norm_map' := ⋯ }

@[simp]

theorem RCLike.conjLIE_apply {K : Type u_1} [RCLike K] : ⇑RCLike.conjLIE = ⇑(starRingEnd K)

noncomputable def RCLike.conjCLE {K : Type u_1} [RCLike K] : K ≃L[ℝ] K

Conjugate as a continuous linear equivalence

Equations

• RCLike.conjCLE = { toLinearEquiv := RCLike.conjLIE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem RCLike.conjCLE_coe {K : Type u_1} [RCLike K] : RCLike.conjCLE.toLinearEquiv = RCLike.conjAe.toLinearEquiv

@[simp]

theorem RCLike.conjCLE_apply {K : Type u_1} [RCLike K] : ⇑RCLike.conjCLE = ⇑(starRingEnd K)

@[instance 100]

instance RCLike.instContinuousStar {K : Type u_1} [RCLike K] : ContinuousStar K

Equations

• ⋯ = ⋯

theorem RCLike.continuous_conj {K : Type u_1} [RCLike K] : Continuous ⇑(starRingEnd K)

noncomputable def RCLike.ofRealAm {K : Type u_1} [RCLike K] : ℝ →ₐ[ℝ] K

The ℝ → K coercion, as a linear map

Equations

• RCLike.ofRealAm = Algebra.ofId ℝ K

@[simp]

theorem RCLike.ofRealAm_coe {K : Type u_1} [RCLike K] : ⇑RCLike.ofRealAm = RCLike.ofReal

noncomputable def RCLike.ofRealLI {K : Type u_1} [RCLike K] : ℝ →ₗᵢ[ℝ] K

The ℝ → K coercion, as a linear isometry

Equations

• RCLike.ofRealLI = { toLinearMap := RCLike.ofRealAm.toLinearMap, norm_map' := ⋯ }

@[simp]

theorem RCLike.ofRealLI_apply {K : Type u_1} [RCLike K] : ⇑RCLike.ofRealLI = RCLike.ofReal

noncomputable def RCLike.ofRealCLM {K : Type u_1} [RCLike K] : ℝ →L[ℝ] K

The ℝ → K coercion, as a continuous linear map

Equations

• RCLike.ofRealCLM = RCLike.ofRealLI.toContinuousLinearMap

@[simp]

theorem RCLike.ofRealCLM_coe {K : Type u_1} [RCLike K] : ↑RCLike.ofRealCLM = RCLike.ofRealAm.toLinearMap

@[simp]

theorem RCLike.ofRealCLM_apply {K : Type u_1} [RCLike K] : ⇑RCLike.ofRealCLM = RCLike.ofReal

theorem RCLike.continuous_ofReal {K : Type u_1} [RCLike K] : Continuous RCLike.ofReal

theorem RCLike.continuous_normSq {K : Type u_1} [RCLike K] : Continuous ⇑RCLike.normSq

ℝ-dependent results

Here we gather results that depend on whether K is ℝ.

theorem RCLike.im_eq_zero {K : Type u_1} [RCLike K] (h : RCLike.I = 0) (z : K) : RCLike.im z = 0

@[simp]

theorem RCLike.realRingEquiv_apply {K : Type u_1} [RCLike K] (h : RCLike.I = 0) (a : K) : (RCLike.realRingEquiv h) a = RCLike.re a

@[simp]

theorem RCLike.realRingEquiv_symm_apply {K : Type u_1} [RCLike K] (h : RCLike.I = 0) : ∀ (a : ℝ), (RCLike.realRingEquiv h).symm a = ↑a

def RCLike.realRingEquiv {K : Type u_1} [RCLike K] (h : RCLike.I = 0) : K ≃+* ℝ

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

Equations

• RCLike.realRingEquiv h = { toFun := ⇑RCLike.re, invFun := RCLike.ofReal, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem RCLike.realLinearIsometryEquiv_symm_apply {K : Type u_1} [RCLike K] (h : RCLike.I = 0) : ∀ (a : ℝ), (RCLike.realLinearIsometryEquiv h).symm a = (RCLike.realRingEquiv h).invFun a

@[simp]

theorem RCLike.realLinearIsometryEquiv_invFun {K : Type u_1} [RCLike K] (h : RCLike.I = 0) : ∀ (a : ℝ), (RCLike.realLinearIsometryEquiv h).invFun a = (RCLike.realRingEquiv h).invFun a

@[simp]

theorem RCLike.realLinearIsometryEquiv_toFun {K : Type u_1} [RCLike K] (h : RCLike.I = 0) : ∀ (a : K), (RCLike.realLinearIsometryEquiv h) a = (RCLike.realRingEquiv h).toFun a

@[simp]

theorem RCLike.realLinearIsometryEquiv_apply {K : Type u_1} [RCLike K] (h : RCLike.I = 0) : ∀ (a : K), (RCLike.realLinearIsometryEquiv h) a = (RCLike.realRingEquiv h).toFun a

noncomputable def RCLike.realLinearIsometryEquiv {K : Type u_1} [RCLike K] (h : RCLike.I = 0) : K ≃ₗᵢ[ℝ] ℝ

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

Equations

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

theorem AddChar.inv_apply_eq_conj {K : Type u_1} [RCLike K] {G : Type u_3} [Finite G] [AddLeftCancelMonoid G] (ψ : AddChar G K) (x : G) : (ψ x)⁻¹ = (starRingEnd K) (ψ x)

theorem AddChar.map_neg_eq_conj {K : Type u_1} [RCLike K] {G : Type u_3} [Finite G] [AddCommGroup G] (ψ : AddChar G K) (x : G) : ψ (-x) = (starRingEnd K) (ψ x)

class IsRCLikeNormedField (𝕜 : Type u_3) [hk : NormedField 𝕜] : Prop

A mixin over a normed field, saying that the norm field structure is the same as ℝ or ℂ. To endow such a field with a compatible RCLike structure in a proof, use letI := IsRCLikeNormedField.rclike 𝕜.

• out : ∃ (h : RCLike 𝕜), hk = DenselyNormedField.toNormedField

theorem IsRCLikeNormedField.out {𝕜 : Type u_3} {hk : NormedField 𝕜} [self : IsRCLikeNormedField 𝕜] : ∃ (h : RCLike 𝕜), hk = DenselyNormedField.toNormedField

@[instance 100]

instance instIsRCLikeNormedField (𝕜 : Type u_3) [h : RCLike 𝕜] : IsRCLikeNormedField 𝕜

Equations

• ⋯ = ⋯

noncomputable def RCLike.copy_of_normedField {𝕜 : Type u_3} (h : RCLike 𝕜) (hk : NormedField 𝕜) (h'' : hk = DenselyNormedField.toNormedField) : RCLike 𝕜

A copy of an RCLike field in which the NormedField field is adjusted to be become defeq to a propeq one.

Equations

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

noncomputable def IsRCLikeNormedField.rclike (𝕜 : Type u_3) [hk : NormedField 𝕜] [h : IsRCLikeNormedField 𝕜] : RCLike 𝕜

Given a normed field 𝕜 satisfying IsRCLikeNormedField 𝕜, build an associated RCLike 𝕜 structure on 𝕜 which is definitionally compatible with the given normed field structure.

Equations

• IsRCLikeNormedField.rclike 𝕜 = (fun (p : RCLike 𝕜) (hp : hk = DenselyNormedField.toNormedField) => p.copy_of_normedField hk hp) (Classical.choose ⋯) ⋯