is_R_or_C: a typeclass for ℝ or ℂ
This file defines the typeclass is_R_or_C 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 ℂ.
Possible applications include defining inner products and Hilbert spaces for both the real and complex case. One would produce 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.
@[class]
- re : K →+ ℝ
- im : K →+ ℝ
- conj : K →+* K
- I : K
- of_real : ℝ → K
- I_re_ax : ⇑is_R_or_C.re is_R_or_C.I = 0
- I_mul_I_ax : is_R_or_C.I = 0 ∨ is_R_or_C.I * is_R_or_C.I = -1
- re_add_im_ax : ∀ (z : K), is_R_or_C.of_real (⇑is_R_or_C.re z) + (is_R_or_C.of_real (⇑is_R_or_C.im z)) * is_R_or_C.I = z
- smul_coe_mul_ax : ∀ (z : K) (r : ℝ), r • z = (is_R_or_C.of_real r) * z
- of_real_re_ax : ∀ (r : ℝ), ⇑is_R_or_C.re (is_R_or_C.of_real r) = r
- of_real_im_ax : ∀ (r : ℝ), ⇑is_R_or_C.im (is_R_or_C.of_real r) = 0
- mul_re_ax : ∀ (z w : K), ⇑is_R_or_C.re (z * w) = (⇑is_R_or_C.re z) * ⇑is_R_or_C.re w - (⇑is_R_or_C.im z) * ⇑is_R_or_C.im w
- mul_im_ax : ∀ (z w : K), ⇑is_R_or_C.im (z * w) = (⇑is_R_or_C.re z) * ⇑is_R_or_C.im w + (⇑is_R_or_C.im z) * ⇑is_R_or_C.re w
- conj_re_ax : ∀ (z : K), ⇑is_R_or_C.re (⇑is_R_or_C.conj z) = ⇑is_R_or_C.re z
- conj_im_ax : ∀ (z : K), ⇑is_R_or_C.im (⇑is_R_or_C.conj z) = -⇑is_R_or_C.im z
- conj_I_ax : ⇑is_R_or_C.conj is_R_or_C.I = -is_R_or_C.I
- norm_sq_eq_def_ax : ∀ (z : K), ∥z∥ ^ 2 = (⇑is_R_or_C.re z) * ⇑is_R_or_C.re z + (⇑is_R_or_C.im z) * ⇑is_R_or_C.im z
- mul_im_I_ax : ∀ (z : K), (⇑is_R_or_C.im z) * ⇑is_R_or_C.im is_R_or_C.I = ⇑is_R_or_C.im z
- inv_def_ax : ∀ (z : K), z⁻¹ = (⇑is_R_or_C.conj z) * is_R_or_C.of_real (∥z∥ ^ 2)⁻¹
- div_I_ax : ∀ (z : K), z / is_R_or_C.I = -z * is_R_or_C.I
This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.
Instances
theorem
is_R_or_C.of_real_alg
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(x : ℝ) :
is_R_or_C.of_real x = x • 1
@[simp]
theorem
is_R_or_C.re_add_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
is_R_or_C.of_real (⇑is_R_or_C.re z) + (is_R_or_C.of_real (⇑is_R_or_C.im z)) * is_R_or_C.I = z
@[simp]
theorem
is_R_or_C.of_real_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
⇑is_R_or_C.re (is_R_or_C.of_real r) = r
@[simp]
theorem
is_R_or_C.of_real_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
⇑is_R_or_C.im (is_R_or_C.of_real r) = 0
@[simp]
theorem
is_R_or_C.mul_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
⇑is_R_or_C.re (z * w) = (⇑is_R_or_C.re z) * ⇑is_R_or_C.re w - (⇑is_R_or_C.im z) * ⇑is_R_or_C.im w
@[simp]
theorem
is_R_or_C.mul_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
⇑is_R_or_C.im (z * w) = (⇑is_R_or_C.re z) * ⇑is_R_or_C.im w + (⇑is_R_or_C.im z) * ⇑is_R_or_C.re w
theorem
is_R_or_C.ext_iff
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z w : K} :
z = w ↔ ⇑is_R_or_C.re z = ⇑is_R_or_C.re w ∧ ⇑is_R_or_C.im z = ⇑is_R_or_C.im w
theorem
is_R_or_C.ext
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z w : K}
(a : ⇑is_R_or_C.re z = ⇑is_R_or_C.re w)
(a_1 : ⇑is_R_or_C.im z = ⇑is_R_or_C.im w) :
z = w
theorem
is_R_or_C.zero_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
⇑is_R_or_C.re (is_R_or_C.of_real 0) = 0
@[simp]
theorem
is_R_or_C.zero_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
⇑is_R_or_C.im (is_R_or_C.of_real 0) = 0
theorem
is_R_or_C.of_real_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
is_R_or_C.of_real 0 = 0
@[simp]
theorem
is_R_or_C.of_real_one
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
is_R_or_C.of_real 1 = 1
@[simp]
theorem
is_R_or_C.one_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
⇑is_R_or_C.re 1 = 1
@[simp]
theorem
is_R_or_C.one_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
⇑is_R_or_C.im 1 = 0
@[simp]
theorem
is_R_or_C.of_real_inj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z w : ℝ} :
is_R_or_C.of_real z = is_R_or_C.of_real w ↔ z = w
@[simp]
theorem
is_R_or_C.bit0_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
⇑is_R_or_C.re (bit0 z) = bit0 (⇑is_R_or_C.re z)
@[simp]
theorem
is_R_or_C.bit1_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
⇑is_R_or_C.re (bit1 z) = bit1 (⇑is_R_or_C.re z)
@[simp]
theorem
is_R_or_C.bit0_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
⇑is_R_or_C.im (bit0 z) = bit0 (⇑is_R_or_C.im z)
@[simp]
theorem
is_R_or_C.bit1_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
⇑is_R_or_C.im (bit1 z) = bit0 (⇑is_R_or_C.im z)
@[simp]
theorem
is_R_or_C.of_real_eq_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : ℝ} :
is_R_or_C.of_real z = 0 ↔ z = 0
@[simp]
theorem
is_R_or_C.of_real_add
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r s : ℝ) :
is_R_or_C.of_real (r + s) = is_R_or_C.of_real r + is_R_or_C.of_real s
@[simp]
theorem
is_R_or_C.of_real_bit0
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
is_R_or_C.of_real (bit0 r) = bit0 (is_R_or_C.of_real r)
@[simp]
theorem
is_R_or_C.of_real_bit1
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
is_R_or_C.of_real (bit1 r) = bit1 (is_R_or_C.of_real r)
theorem
is_R_or_C.two_ne_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
2 ≠ 0
@[simp]
theorem
is_R_or_C.of_real_neg
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
@[simp]
theorem
is_R_or_C.of_real_mul
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r s : ℝ) :
is_R_or_C.of_real (r * s) = (is_R_or_C.of_real r) * is_R_or_C.of_real s
theorem
is_R_or_C.smul_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ)
(z : K) :
⇑is_R_or_C.re ((is_R_or_C.of_real r) * z) = r * ⇑is_R_or_C.re z
theorem
is_R_or_C.smul_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ)
(z : K) :
⇑is_R_or_C.im ((is_R_or_C.of_real r) * z) = r * ⇑is_R_or_C.im z
theorem
is_R_or_C.smul_re'
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ)
(z : K) :
⇑is_R_or_C.re (r • z) = r * ⇑is_R_or_C.re z
theorem
is_R_or_C.smul_im'
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ)
(z : K) :
⇑is_R_or_C.im (r • z) = r * ⇑is_R_or_C.im z
The imaginary unit, I
@[simp]
The imaginary unit.
@[simp]
theorem
is_R_or_C.I_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
theorem
is_R_or_C.I_mul_I
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
is_R_or_C.I = 0 ∨ is_R_or_C.I * is_R_or_C.I = -1
@[simp]
theorem
is_R_or_C.conj_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
@[simp]
theorem
is_R_or_C.conj_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
@[simp]
theorem
is_R_or_C.conj_of_real
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
@[simp]
theorem
is_R_or_C.conj_bit0
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
⇑is_R_or_C.conj (bit0 z) = bit0 (⇑is_R_or_C.conj z)
@[simp]
theorem
is_R_or_C.conj_bit1
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
⇑is_R_or_C.conj (bit1 z) = bit1 (⇑is_R_or_C.conj z)
@[simp]
theorem
is_R_or_C.conj_neg_I
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
@[simp]
theorem
is_R_or_C.conj_conj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
⇑is_R_or_C.conj (⇑is_R_or_C.conj z) = z
theorem
is_R_or_C.conj_involutive
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
theorem
is_R_or_C.conj_bijective
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
theorem
is_R_or_C.conj_inj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
⇑is_R_or_C.conj z = ⇑is_R_or_C.conj w ↔ z = w
@[simp]
theorem
is_R_or_C.conj_eq_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
⇑is_R_or_C.conj z = 0 ↔ z = 0
theorem
is_R_or_C.eq_conj_iff_real
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
⇑is_R_or_C.conj z = z ↔ ∃ (r : ℝ), z = is_R_or_C.of_real r
theorem
is_R_or_C.eq_conj_iff_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
⇑is_R_or_C.conj z = z ↔ is_R_or_C.of_real (⇑is_R_or_C.re z) = z
def
is_R_or_C.norm_sq
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
The norm squared function.
Equations
- is_R_or_C.norm_sq z = (⇑is_R_or_C.re z) * ⇑is_R_or_C.re z + (⇑is_R_or_C.im z) * ⇑is_R_or_C.im z
theorem
is_R_or_C.norm_sq_eq_def
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
∥z∥ ^ 2 = (⇑is_R_or_C.re z) * ⇑is_R_or_C.re z + (⇑is_R_or_C.im z) * ⇑is_R_or_C.im z
theorem
is_R_or_C.norm_sq_eq_def'
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
is_R_or_C.norm_sq z = ∥z∥ ^ 2
@[simp]
theorem
is_R_or_C.norm_sq_of_real
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
@[simp]
theorem
is_R_or_C.norm_sq_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
is_R_or_C.norm_sq 0 = 0
@[simp]
theorem
is_R_or_C.norm_sq_one
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
is_R_or_C.norm_sq 1 = 1
theorem
is_R_or_C.norm_sq_nonneg
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
0 ≤ is_R_or_C.norm_sq z
@[simp]
theorem
is_R_or_C.norm_sq_eq_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
is_R_or_C.norm_sq z = 0 ↔ z = 0
@[simp]
theorem
is_R_or_C.norm_sq_pos
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
0 < is_R_or_C.norm_sq z ↔ z ≠ 0
@[simp]
theorem
is_R_or_C.norm_sq_neg
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
@[simp]
theorem
is_R_or_C.norm_sq_conj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
@[simp]
theorem
is_R_or_C.norm_sq_mul
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
is_R_or_C.norm_sq (z * w) = (is_R_or_C.norm_sq z) * is_R_or_C.norm_sq w
theorem
is_R_or_C.norm_sq_add
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
is_R_or_C.norm_sq (z + w) = is_R_or_C.norm_sq z + is_R_or_C.norm_sq w + 2 * ⇑is_R_or_C.re (z * ⇑is_R_or_C.conj w)
theorem
is_R_or_C.re_sq_le_norm_sq
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
(⇑is_R_or_C.re z) * ⇑is_R_or_C.re z ≤ is_R_or_C.norm_sq z
theorem
is_R_or_C.im_sq_le_norm_sq
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
(⇑is_R_or_C.im z) * ⇑is_R_or_C.im z ≤ is_R_or_C.norm_sq z
theorem
is_R_or_C.mul_conj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
theorem
is_R_or_C.add_conj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
z + ⇑is_R_or_C.conj z = is_R_or_C.of_real (2 * ⇑is_R_or_C.re z)
The pseudo-coercion of_real as a ring_hom.
Equations
- is_R_or_C.of_real_hom = {to_fun := is_R_or_C.of_real _inst_3, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
is_R_or_C.of_real_sub
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r s : ℝ) :
is_R_or_C.of_real (r - s) = is_R_or_C.of_real r - is_R_or_C.of_real s
@[simp]
theorem
is_R_or_C.of_real_pow
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ)
(n : ℕ) :
is_R_or_C.of_real (r ^ n) = is_R_or_C.of_real r ^ n
theorem
is_R_or_C.sub_conj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
z - ⇑is_R_or_C.conj z = (is_R_or_C.of_real (2 * ⇑is_R_or_C.im z)) * is_R_or_C.I
theorem
is_R_or_C.norm_sq_sub
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
is_R_or_C.norm_sq (z - w) = is_R_or_C.norm_sq z + is_R_or_C.norm_sq w - 2 * ⇑is_R_or_C.re (z * ⇑is_R_or_C.conj w)
Inversion
theorem
is_R_or_C.inv_def
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
z⁻¹ = (⇑is_R_or_C.conj z) * is_R_or_C.of_real (∥z∥ ^ 2)⁻¹
@[simp]
theorem
is_R_or_C.inv_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
@[simp]
theorem
is_R_or_C.inv_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
⇑is_R_or_C.im z⁻¹ = ⇑is_R_or_C.im (-z) / is_R_or_C.norm_sq z
@[simp]
theorem
is_R_or_C.of_real_inv
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
theorem
is_R_or_C.inv_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
theorem
is_R_or_C.mul_inv_cancel
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K}
(h : z ≠ 0) :
theorem
is_R_or_C.div_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
⇑is_R_or_C.re (z / w) = (⇑is_R_or_C.re z) * ⇑is_R_or_C.re w / is_R_or_C.norm_sq w + (⇑is_R_or_C.im z) * ⇑is_R_or_C.im w / is_R_or_C.norm_sq w
theorem
is_R_or_C.div_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
⇑is_R_or_C.im (z / w) = (⇑is_R_or_C.im z) * ⇑is_R_or_C.re w / is_R_or_C.norm_sq w - (⇑is_R_or_C.re z) * ⇑is_R_or_C.im w / is_R_or_C.norm_sq w
@[simp]
theorem
is_R_or_C.of_real_div
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r s : ℝ) :
is_R_or_C.of_real (r / s) = is_R_or_C.of_real r / is_R_or_C.of_real s
@[simp]
theorem
is_R_or_C.of_real_fpow
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ)
(n : ℤ) :
is_R_or_C.of_real (r ^ n) = is_R_or_C.of_real r ^ n
theorem
is_R_or_C.I_mul_I_of_nonzero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(a : is_R_or_C.I ≠ 0) :
is_R_or_C.I * is_R_or_C.I = -1
@[simp]
theorem
is_R_or_C.div_I
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
z / is_R_or_C.I = -z * is_R_or_C.I
@[simp]
@[simp]
theorem
is_R_or_C.norm_sq_inv
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
@[simp]
theorem
is_R_or_C.norm_sq_div
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
is_R_or_C.norm_sq (z / w) = is_R_or_C.norm_sq z / is_R_or_C.norm_sq w
Cast lemmas
@[simp]
theorem
is_R_or_C.of_real_nat_cast
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℕ) :
is_R_or_C.of_real ↑n = ↑n
@[simp]
theorem
is_R_or_C.nat_cast_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℕ) :
⇑is_R_or_C.re ↑n = ↑n
@[simp]
theorem
is_R_or_C.nat_cast_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℕ) :
⇑is_R_or_C.im ↑n = 0
@[simp]
theorem
is_R_or_C.of_real_int_cast
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℤ) :
is_R_or_C.of_real ↑n = ↑n
@[simp]
theorem
is_R_or_C.int_cast_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℤ) :
⇑is_R_or_C.re ↑n = ↑n
@[simp]
theorem
is_R_or_C.int_cast_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℤ) :
⇑is_R_or_C.im ↑n = 0
@[simp]
theorem
is_R_or_C.of_real_rat_cast
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℚ) :
is_R_or_C.of_real ↑n = ↑n
@[simp]
theorem
is_R_or_C.rat_cast_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(q : ℚ) :
⇑is_R_or_C.re ↑q = ↑q
@[simp]
theorem
is_R_or_C.rat_cast_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(q : ℚ) :
⇑is_R_or_C.im ↑q = 0
Characteristic zero
theorem
is_R_or_C.char_zero_R_or_C
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
ℝ and ℂ are both of characteristic zero.
Note: This is not registered as an instance to avoid having multiple instances on ℝ and ℂ.
theorem
is_R_or_C.re_eq_add_conj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
is_R_or_C.of_real (⇑is_R_or_C.re z) = (z + ⇑is_R_or_C.conj z) / 2
Absolute value
The complex absolute value function, defined as the square root of the norm squared.
Equations
@[simp]
theorem
is_R_or_C.abs_of_real
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(r : ℝ) :
is_R_or_C.abs (is_R_or_C.of_real r) = abs r
theorem
is_R_or_C.abs_of_nonneg
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{r : ℝ}
(h : 0 ≤ r) :
is_R_or_C.abs (is_R_or_C.of_real r) = r
theorem
is_R_or_C.abs_of_nat
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℕ) :
is_R_or_C.abs ↑n = ↑n
theorem
is_R_or_C.mul_self_abs
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
(is_R_or_C.abs z) * is_R_or_C.abs z = is_R_or_C.norm_sq z
@[simp]
theorem
is_R_or_C.abs_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
is_R_or_C.abs 0 = 0
@[simp]
theorem
is_R_or_C.abs_one
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
is_R_or_C.abs 1 = 1
@[simp]
theorem
is_R_or_C.abs_two
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
is_R_or_C.abs 2 = 2
theorem
is_R_or_C.abs_nonneg
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
0 ≤ is_R_or_C.abs z
@[simp]
theorem
is_R_or_C.abs_eq_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
is_R_or_C.abs z = 0 ↔ z = 0
theorem
is_R_or_C.abs_ne_zero
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
is_R_or_C.abs z ≠ 0 ↔ z ≠ 0
@[simp]
theorem
is_R_or_C.abs_conj
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
@[simp]
theorem
is_R_or_C.abs_mul
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
is_R_or_C.abs (z * w) = (is_R_or_C.abs z) * is_R_or_C.abs w
theorem
is_R_or_C.abs_re_le_abs
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
abs (⇑is_R_or_C.re z) ≤ is_R_or_C.abs z
theorem
is_R_or_C.abs_im_le_abs
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
abs (⇑is_R_or_C.im z) ≤ is_R_or_C.abs z
theorem
is_R_or_C.re_le_abs
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
theorem
is_R_or_C.im_le_abs
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
theorem
is_R_or_C.abs_add
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
is_R_or_C.abs (z + w) ≤ is_R_or_C.abs z + is_R_or_C.abs w
@[instance]
def
is_R_or_C.is_absolute_value
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K] :
@[simp]
theorem
is_R_or_C.abs_abs
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
abs (is_R_or_C.abs z) = is_R_or_C.abs z
@[simp]
theorem
is_R_or_C.abs_pos
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{z : K} :
0 < is_R_or_C.abs z ↔ z ≠ 0
@[simp]
theorem
is_R_or_C.abs_neg
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
is_R_or_C.abs (-z) = is_R_or_C.abs z
theorem
is_R_or_C.abs_sub
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
is_R_or_C.abs (z - w) = is_R_or_C.abs (w - z)
theorem
is_R_or_C.abs_sub_le
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(a b c : K) :
is_R_or_C.abs (a - c) ≤ is_R_or_C.abs (a - b) + is_R_or_C.abs (b - c)
@[simp]
theorem
is_R_or_C.abs_inv
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
is_R_or_C.abs z⁻¹ = (is_R_or_C.abs z)⁻¹
@[simp]
theorem
is_R_or_C.abs_div
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
is_R_or_C.abs (z / w) = is_R_or_C.abs z / is_R_or_C.abs w
theorem
is_R_or_C.abs_abs_sub_le_abs_sub
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z w : K) :
abs (is_R_or_C.abs z - is_R_or_C.abs w) ≤ is_R_or_C.abs (z - w)
theorem
is_R_or_C.abs_re_div_abs_le_one
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
abs (⇑is_R_or_C.re z / is_R_or_C.abs z) ≤ 1
theorem
is_R_or_C.abs_im_div_abs_le_one
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(z : K) :
abs (⇑is_R_or_C.im z / is_R_or_C.abs z) ≤ 1
@[simp]
theorem
is_R_or_C.abs_cast_nat
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(n : ℕ) :
is_R_or_C.abs ↑n = ↑n
theorem
is_R_or_C.norm_sq_eq_abs
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(x : K) :
is_R_or_C.norm_sq x = is_R_or_C.abs x ^ 2
Cauchy sequences
theorem
is_R_or_C.is_cau_seq_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(f : cau_seq K is_R_or_C.abs) :
is_cau_seq abs (λ (n : ℕ), ⇑is_R_or_C.re (⇑f n))
theorem
is_R_or_C.is_cau_seq_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(f : cau_seq K is_R_or_C.abs) :
is_cau_seq abs (λ (n : ℕ), ⇑is_R_or_C.im (⇑f n))
def
is_R_or_C.cau_seq_re
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(f : cau_seq K is_R_or_C.abs) :
The real part of a K Cauchy sequence, as a real Cauchy sequence.
Equations
- is_R_or_C.cau_seq_re f = ⟨λ (n : ℕ), ⇑is_R_or_C.re (⇑f n), _⟩
def
is_R_or_C.cau_seq_im
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
(f : cau_seq K is_R_or_C.abs) :
The imaginary part of a K Cauchy sequence, as a real Cauchy sequence.
Equations
- is_R_or_C.cau_seq_im f = ⟨λ (n : ℕ), ⇑is_R_or_C.im (⇑f n), _⟩
theorem
is_R_or_C.is_cau_seq_abs
{K : Type u_1}
[nondiscrete_normed_field K]
[algebra ℝ K]
[is_R_or_C K]
{f : ℕ → K}
(hf : is_cau_seq is_R_or_C.abs f) :
is_cau_seq abs (is_R_or_C.abs ∘ f)
@[instance]
Equations
- real.is_R_or_C = {re := add_monoid_hom.id ℝ (add_group.to_add_monoid ℝ), im := 0, conj := ring_hom.id ℝ ring.to_semiring, I := 0, of_real := id ℝ, I_re_ax := real.is_R_or_C._proof_1, I_mul_I_ax := real.is_R_or_C._proof_2, re_add_im_ax := real.is_R_or_C._proof_3, smul_coe_mul_ax := real.is_R_or_C._proof_4, of_real_re_ax := real.is_R_or_C._proof_5, of_real_im_ax := real.is_R_or_C._proof_6, mul_re_ax := real.is_R_or_C._proof_7, mul_im_ax := real.is_R_or_C._proof_8, conj_re_ax := real.is_R_or_C._proof_9, conj_im_ax := real.is_R_or_C._proof_10, conj_I_ax := real.is_R_or_C._proof_11, norm_sq_eq_def_ax := real.is_R_or_C._proof_12, mul_im_I_ax := real.is_R_or_C._proof_13, inv_def_ax := real.is_R_or_C._proof_14, div_I_ax := real.is_R_or_C._proof_15}
@[instance]
Equations
- complex.is_R_or_C = {re := {to_fun := complex.re, map_zero' := complex.zero_re, map_add' := complex.add_re}, im := {to_fun := complex.im, map_zero' := complex.zero_im, map_add' := complex.add_im}, conj := complex.conj, I := complex.I, of_real := coe coe_to_lift, I_re_ax := complex.is_R_or_C._proof_1, I_mul_I_ax := complex.is_R_or_C._proof_2, re_add_im_ax := complex.is_R_or_C._proof_3, smul_coe_mul_ax := complex.is_R_or_C._proof_4, of_real_re_ax := complex.is_R_or_C._proof_5, of_real_im_ax := complex.is_R_or_C._proof_6, mul_re_ax := complex.is_R_or_C._proof_7, mul_im_ax := complex.is_R_or_C._proof_8, conj_re_ax := complex.is_R_or_C._proof_9, conj_im_ax := complex.is_R_or_C._proof_10, conj_I_ax := complex.is_R_or_C._proof_11, norm_sq_eq_def_ax := complex.is_R_or_C._proof_12, mul_im_I_ax := complex.is_R_or_C._proof_13, inv_def_ax := complex.is_R_or_C._proof_14, div_I_ax := complex.div_I}
@[simp]