Extra lemmas on RCLike

This file contains extra lemmas on RCLike.

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

Alias of RCLike.le_iff_re_im.

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

Alias of RCLike.lt_iff_re_im.

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

Alias of RCLike.nonneg_iff.

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

Alias of RCLike.pos_iff.

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

Alias of RCLike.nonpos_iff.

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

Alias of RCLike.neg_iff.

theorem RCLike.nonneg_def' {𝕜 : Type u_1} [RCLike 𝕜] {x : 𝕜} : 0 ≤ x ↔ ↑(re x) = x ∧ 0 ≤ re x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem RCLike.not_le_iff {𝕜 : Type u_1} [RCLike 𝕜] {z w : 𝕜} : ¬z ≤ w ↔ re w < re z ∨ im z ≠ im w

theorem RCLike.not_lt_iff {𝕜 : Type u_1} [RCLike 𝕜] {z w : 𝕜} : ¬z < w ↔ re w ≤ re z ∨ im z ≠ im w

theorem RCLike.not_le_zero_iff {𝕜 : Type u_1} [RCLike 𝕜] {z : 𝕜} : ¬z ≤ 0 ↔ 0 < re z ∨ im z ≠ 0

theorem RCLike.not_lt_zero_iff {𝕜 : Type u_1} [RCLike 𝕜] {z : 𝕜} : ¬z < 0 ↔ 0 ≤ re z ∨ im z ≠ 0

theorem RCLike.eq_re_ofReal_le {𝕜 : Type u_1} [RCLike 𝕜] {r : ℝ} {z : 𝕜} (hz : ↑r ≤ z) : z = ↑(re z)