data.complex.basic - mathlib3 docs

complex.equiv_real_prod = {to_fun := λ (z : ℂ), (z.re, z.im), inv_fun := λ (p : ℝ × ℝ), {re := p.fst, im := p.snd}, left_inv := complex.equiv_real_prod._proof_1, right_inv := complex.equiv_real_prod._proof_2}

source

@[simp]

theorem complex.eta (z : ℂ) :

{re := z.re, im := z.im} = z

source

@[ext]

theorem complex.ext {z w : ℂ} :

z.re = w.re → z.im = w.im → z = w

source

theorem complex.ext_iff {z w : ℂ} :

z = w ↔ z.re = w.re ∧ z.im = w.im

source

theorem complex.re_surjective :

function.surjective complex.re

source

theorem complex.im_surjective :

function.surjective complex.im

source

@[simp]

theorem complex.range_re :

set.range complex.re = set.univ

source

@[simp]

theorem complex.range_im :

set.range complex.im = set.univ

source

@[protected, instance]

def complex.has_coe :

has_coe ℝ ℂ

Equations

complex.has_coe = {coe := λ (r : ℝ), {re := r, im := 0}}

source

@[simp, norm_cast]

theorem complex.of_real_re (r : ℝ) :

↑r.re = r

source

@[simp, norm_cast]

theorem complex.of_real_im (r : ℝ) :

↑r.im = 0

source

theorem complex.of_real_def (r : ℝ) :

↑r = {re := r, im := 0}

source

@[simp, norm_cast]

theorem complex.of_real_inj {z w : ℝ} :

↑z = ↑w ↔ z = w

source

theorem complex.of_real_injective :

function.injective coe

source

@[protected, instance]

def complex.can_lift :

can_lift ℂ ℝ coe (λ (z : ℂ), z.im = 0)

Equations

complex.can_lift = {prf := complex.can_lift._proof_1}

source

def set.re_prod_im (s t : set ℝ) :

set ℂ

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

Equations

s ×ℂ t = complex.re ⁻¹' s ∩ complex.im ⁻¹' t

source

theorem complex.mem_re_prod_im {z : ℂ} {s t : set ℝ} :

z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t

source

@[protected, instance]

def complex.has_zero :

has_zero ℂ

Equations

complex.has_zero = {zero := ↑0}

source

@[protected, instance]

def complex.inhabited :

inhabited ℂ

Equations

complex.inhabited = {default := 0}

source

@[simp]

theorem complex.zero_re :

0.re = 0

source

@[simp]

theorem complex.zero_im :

0.im = 0

source

@[simp, norm_cast]

theorem complex.of_real_zero :

↑0 = 0

source

@[simp]

theorem complex.of_real_eq_zero {z : ℝ} :

↑z = 0 ↔ z = 0

source

theorem complex.of_real_ne_zero {z : ℝ} :

↑z ≠ 0 ↔ z ≠ 0

source

@[protected, instance]

def complex.has_one :

has_one ℂ

Equations

complex.has_one = {one := ↑1}

source

@[simp]

theorem complex.one_re :

1.re = 1

source

@[simp]

theorem complex.one_im :

1.im = 0

source

@[simp, norm_cast]

theorem complex.of_real_one :

↑1 = 1

source

@[simp]

theorem complex.of_real_eq_one {z : ℝ} :

↑z = 1 ↔ z = 1

source

theorem complex.of_real_ne_one {z : ℝ} :

↑z ≠ 1 ↔ z ≠ 1

source

@[protected, instance]

def complex.has_add :

has_add ℂ

Equations

complex.has_add = {add := λ (z w : ℂ), {re := z.re + w.re, im := z.im + w.im}}

source

@[simp]

theorem complex.add_re (z w : ℂ) :

(z + w).re = z.re + w.re

source

@[simp]

theorem complex.add_im (z w : ℂ) :

(z + w).im = z.im + w.im

source

@[simp]

theorem complex.bit0_re (z : ℂ) :

(bit0 z).re = bit0 z.re

source

@[simp]

theorem complex.bit1_re (z : ℂ) :

(bit1 z).re = bit1 z.re

source

@[simp]

theorem complex.bit0_im (z : ℂ) :

(bit0 z).im = bit0 z.im

source

@[simp]

theorem complex.bit1_im (z : ℂ) :

(bit1 z).im = bit0 z.im

source

@[simp, norm_cast]

theorem complex.of_real_add (r s : ℝ) :

↑(r + s) = ↑r + ↑s

source

@[simp, norm_cast]

theorem complex.of_real_bit0 (r : ℝ) :

↑(bit0 r) = bit0 ↑r

source

@[simp, norm_cast]

theorem complex.of_real_bit1 (r : ℝ) :

↑(bit1 r) = bit1 ↑r

source

@[protected, instance]

def complex.has_neg :

has_neg ℂ

Equations

complex.has_neg = {neg := λ (z : ℂ), {re := -z.re, im := -z.im}}

source

@[simp]

theorem complex.neg_re (z : ℂ) :

(-z).re = -z.re

source

@[simp]

theorem complex.neg_im (z : ℂ) :

(-z).im = -z.im

source

@[simp, norm_cast]

theorem complex.of_real_neg (r : ℝ) :

↑-r = -↑r

source

@[protected, instance]

def complex.has_sub :

has_sub ℂ

Equations

complex.has_sub = {sub := λ (z w : ℂ), {re := z.re - w.re, im := z.im - w.im}}

source

@[protected, instance]

def complex.has_mul :

has_mul ℂ

Equations

complex.has_mul = {mul := λ (z w : ℂ), {re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re}}

source

@[simp]

theorem complex.mul_re (z w : ℂ) :

(z * w).re = z.re * w.re - z.im * w.im

source

@[simp]

theorem complex.mul_im (z w : ℂ) :

(z * w).im = z.re * w.im + z.im * w.re

source

@[simp, norm_cast]

theorem complex.of_real_mul (r s : ℝ) :

↑(r * s) = ↑r * ↑s

source

theorem complex.of_real_mul_re (r : ℝ) (z : ℂ) :

(↑r * z).re = r * z.re

source

theorem complex.of_real_mul_im (r : ℝ) (z : ℂ) :

(↑r * z).im = r * z.im

source

theorem complex.of_real_mul' (r : ℝ) (z : ℂ) :

↑r * z = {re := r * z.re, im := r * z.im}

source

def complex.I :

ℂ

The imaginary unit.

Equations

complex.I = {re := 0, im := 1}

source

@[simp]

theorem complex.I_re :

complex.I.re = 0

source

@[simp]

theorem complex.I_im :

complex.I.im = 1

source

@[simp]

theorem complex.I_mul_I :

complex.I * complex.I = -1

source

theorem complex.I_mul (z : ℂ) :

complex.I * z = {re := -z.im, im := z.re}

source

theorem complex.I_ne_zero :

complex.I ≠ 0

source

theorem complex.mk_eq_add_mul_I (a b : ℝ) :

{re := a, im := b} = ↑a + ↑b * complex.I

source

@[simp]

theorem complex.re_add_im (z : ℂ) :

↑(z.re) + ↑(z.im) * complex.I = z

source

theorem complex.mul_I_re (z : ℂ) :

(z * complex.I).re = -z.im

source

theorem complex.mul_I_im (z : ℂ) :

(z * complex.I).im = z.re

source

theorem complex.I_mul_re (z : ℂ) :

(complex.I * z).re = -z.im

source

theorem complex.I_mul_im (z : ℂ) :

(complex.I * z).im = z.re

source

@[simp]

theorem complex.equiv_real_prod_symm_apply (p : ℝ × ℝ) :

⇑(complex.equiv_real_prod.symm) p = ↑(p.fst) + ↑(p.snd) * complex.I

source

@[protected, instance]

def complex.nontrivial :

nontrivial ℂ

source

@[protected, instance]

def complex.add_comm_group :

add_comm_group ℂ

Equations

complex.add_comm_group = {add := has_add.add complex.has_add, add_assoc := complex.add_comm_group._proof_1, zero := 0, zero_add := complex.add_comm_group._proof_2, add_zero := complex.add_comm_group._proof_3, nsmul := λ (n : ℕ) (z : ℂ), {re := n • z.re - 0 * z.im, im := n • z.im + 0 * z.re}, nsmul_zero' := complex.add_comm_group._proof_4, nsmul_succ' := complex.add_comm_group._proof_5, neg := has_neg.neg complex.has_neg, sub := has_sub.sub complex.has_sub, sub_eq_add_neg := complex.add_comm_group._proof_6, zsmul := λ (n : ℤ) (z : ℂ), {re := n • z.re - 0 * z.im, im := n • z.im + 0 * z.re}, zsmul_zero' := complex.add_comm_group._proof_7, zsmul_succ' := complex.add_comm_group._proof_8, zsmul_neg' := complex.add_comm_group._proof_9, add_left_neg := complex.add_comm_group._proof_10, add_comm := complex.add_comm_group._proof_11}

source

@[protected, instance]

def complex.add_group_with_one :

add_group_with_one ℂ

Equations

complex.add_group_with_one = {int_cast := λ (n : ℤ), {re := ↑n, im := 0}, add := add_comm_group.add complex.add_comm_group, add_assoc := _, zero := add_comm_group.zero complex.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul complex.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg complex.add_comm_group, sub := add_comm_group.sub complex.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul complex.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := λ (n : ℕ), {re := ↑n, im := 0}, one := 1, nat_cast_zero := complex.add_group_with_one._proof_1, nat_cast_succ := complex.add_group_with_one._proof_2, int_cast_of_nat := complex.add_group_with_one._proof_3, int_cast_neg_succ_of_nat := complex.add_group_with_one._proof_4}

source

@[protected, instance]

def complex.comm_ring :

comm_ring ℂ

Equations

complex.comm_ring = {add := has_add.add complex.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul complex.add_group_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg complex.add_group_with_one, sub := add_group_with_one.sub complex.add_group_with_one, sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul complex.add_group_with_one, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := complex.comm_ring._proof_1, int_cast := add_group_with_one.int_cast complex.add_group_with_one, nat_cast := add_group_with_one.nat_cast complex.add_group_with_one, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul complex.has_mul, mul_assoc := complex.comm_ring._proof_2, one_mul := complex.comm_ring._proof_3, mul_one := complex.comm_ring._proof_4, npow := npow_rec {mul := has_mul.mul complex.has_mul}, npow_zero' := complex.comm_ring._proof_5, npow_succ' := complex.comm_ring._proof_6, left_distrib := complex.comm_ring._proof_7, right_distrib := complex.comm_ring._proof_8, mul_comm := complex.comm_ring._proof_9}

source

@[protected, instance]

def complex.ring :

ring ℂ

This shortcut instance ensures we do not find ring via the noncomputable complex.field instance.

Equations

complex.ring = comm_ring.to_ring ℂ

source

@[protected, instance]

def complex.comm_semiring :

comm_semiring ℂ

This shortcut instance ensures we do not find comm_semiring via the noncomputable complex.field instance.

Equations

complex.comm_semiring = infer_instance

source

def complex.re_add_group_hom :

ℂ →+ ℝ

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

Equations

complex.re_add_group_hom = {to_fun := complex.re, map_zero' := complex.zero_re, map_add' := complex.add_re}

source

@[simp]

theorem complex.coe_re_add_group_hom :

⇑complex.re_add_group_hom = complex.re

source

def complex.im_add_group_hom :

ℂ →+ ℝ

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

Equations

complex.im_add_group_hom = {to_fun := complex.im, map_zero' := complex.zero_im, map_add' := complex.add_im}

source

@[simp]

theorem complex.coe_im_add_group_hom :

⇑complex.im_add_group_hom = complex.im

source

@[simp]

theorem complex.I_pow_bit0 (n : ℕ) :

complex.I ^ bit0 n = (-1) ^ n

source

@[simp]

theorem complex.I_pow_bit1 (n : ℕ) :

complex.I ^ bit1 n = (-1) ^ n * complex.I

source

@[protected, instance]

def complex.star_ring :

star_ring ℂ

This defines the complex conjugate as the star operation of the star_ring ℂ. It is recommended to use the ring endomorphism version star_ring_end, available under the notation conj in the locale complex_conjugate.

Equations

complex.star_ring = {to_star_semigroup := {to_has_involutive_star := {to_has_star := {star := λ (z : ℂ), {re := z.re, im := -z.im}}, star_involutive := complex.star_ring._proof_1}, star_mul := complex.star_ring._proof_2}, star_add := complex.star_ring._proof_3}

source

@[simp]

theorem complex.conj_re (z : ℂ) :

(⇑(star_ring_end ℂ) z).re = z.re

source

@[simp]

theorem complex.conj_im (z : ℂ) :

(⇑(star_ring_end ℂ) z).im = -z.im

source

theorem complex.conj_of_real (r : ℝ) :

⇑(star_ring_end ℂ) ↑r = ↑r

source

@[simp]

theorem complex.conj_I :

⇑(star_ring_end ℂ) complex.I = -complex.I

source

theorem complex.conj_bit0 (z : ℂ) :

⇑(star_ring_end ℂ) (bit0 z) = bit0 (⇑(star_ring_end ℂ) z)

source

theorem complex.conj_bit1 (z : ℂ) :

⇑(star_ring_end ℂ) (bit1 z) = bit1 (⇑(star_ring_end ℂ) z)

source

@[simp]

theorem complex.conj_neg_I :

⇑(star_ring_end ℂ) (-complex.I) = complex.I

source

theorem complex.conj_eq_iff_real {z : ℂ} :

⇑(star_ring_end ℂ) z = z ↔ ∃ (r : ℝ), z = ↑r

source

theorem complex.conj_eq_iff_re {z : ℂ} :

⇑(star_ring_end ℂ) z = z ↔ ↑(z.re) = z

source

theorem complex.conj_eq_iff_im {z : ℂ} :

⇑(star_ring_end ℂ) z = z ↔ z.im = 0

source

@[simp, nolint]

theorem complex.star_def :

has_star.star = ⇑(star_ring_end ℂ)

source

def complex.norm_sq :

ℂ →*₀ ℝ

The norm squared function.

Equations

complex.norm_sq = {to_fun := λ (z : ℂ), z.re * z.re + z.im * z.im, map_zero' := complex.norm_sq._proof_1, map_one' := complex.norm_sq._proof_2, map_mul' := complex.norm_sq._proof_3}

source

theorem complex.norm_sq_apply (z : ℂ) :

⇑complex.norm_sq z = z.re * z.re + z.im * z.im

source

@[simp]

theorem complex.norm_sq_of_real (r : ℝ) :

⇑complex.norm_sq ↑r = r * r

source

@[simp]

theorem complex.norm_sq_mk (x y : ℝ) :

⇑complex.norm_sq {re := x, im := y} = x * x + y * y

source

theorem complex.norm_sq_add_mul_I (x y : ℝ) :

⇑complex.norm_sq (↑x + ↑y * complex.I) = x ^ 2 + y ^ 2

source

theorem complex.norm_sq_eq_conj_mul_self {z : ℂ} :

↑(⇑complex.norm_sq z) = ⇑(star_ring_end ℂ) z * z

source

@[simp]

theorem complex.norm_sq_zero :

⇑complex.norm_sq 0 = 0

source

@[simp]

theorem complex.norm_sq_one :

⇑complex.norm_sq 1 = 1

source

@[simp]

theorem complex.norm_sq_I :

⇑complex.norm_sq complex.I = 1

source

theorem complex.norm_sq_nonneg (z : ℂ) :

0 ≤ ⇑complex.norm_sq z

source

@[simp]

theorem complex.range_norm_sq :

set.range ⇑complex.norm_sq = set.Ici 0

source

theorem complex.norm_sq_eq_zero {z : ℂ} :

⇑complex.norm_sq z = 0 ↔ z = 0

source

@[simp]

theorem complex.norm_sq_pos {z : ℂ} :

0 < ⇑complex.norm_sq z ↔ z ≠ 0

source

@[simp]

theorem complex.norm_sq_neg (z : ℂ) :

⇑complex.norm_sq (-z) = ⇑complex.norm_sq z

source

@[simp]

theorem complex.norm_sq_conj (z : ℂ) :

⇑complex.norm_sq (⇑(star_ring_end ℂ) z) = ⇑complex.norm_sq z

source

theorem complex.norm_sq_mul (z w : ℂ) :

⇑complex.norm_sq (z * w) = ⇑complex.norm_sq z * ⇑complex.norm_sq w

source

theorem complex.norm_sq_add (z w : ℂ) :

⇑complex.norm_sq (z + w) = ⇑complex.norm_sq z + ⇑complex.norm_sq w + 2 * (z * ⇑(star_ring_end ℂ) w).re

source

theorem complex.re_sq_le_norm_sq (z : ℂ) :

z.re * z.re ≤ ⇑complex.norm_sq z

source

theorem complex.im_sq_le_norm_sq (z : ℂ) :

z.im * z.im ≤ ⇑complex.norm_sq z

source

theorem complex.mul_conj (z : ℂ) :

z * ⇑(star_ring_end ℂ) z = ↑(⇑complex.norm_sq z)

source

theorem complex.add_conj (z : ℂ) :

z + ⇑(star_ring_end ℂ) z = ↑(2 * z.re)

source

def complex.of_real :

ℝ →+* ℂ

The coercion ℝ → ℂ as a ring_hom.

Equations

complex.of_real = {to_fun := coe coe_to_lift, map_one' := complex.of_real_one, map_mul' := complex.of_real_mul, map_zero' := complex.of_real_zero, map_add' := complex.of_real_add}

source

@[simp]

theorem complex.of_real_eq_coe (r : ℝ) :

⇑complex.of_real r = ↑r

source

@[simp]

theorem complex.I_sq :

complex.I ^ 2 = -1

source

@[simp]

theorem complex.sub_re (z w : ℂ) :

(z - w).re = z.re - w.re

source

@[simp]

theorem complex.sub_im (z w : ℂ) :

(z - w).im = z.im - w.im

source

@[simp, norm_cast]

theorem complex.of_real_sub (r s : ℝ) :

↑(r - s) = ↑r - ↑s

source

@[simp, norm_cast]

theorem complex.of_real_pow (r : ℝ) (n : ℕ) :

↑(r ^ n) = ↑r ^ n

source

theorem complex.sub_conj (z : ℂ) :

z - ⇑(star_ring_end ℂ) z = ↑(2 * z.im) * complex.I

source

theorem complex.norm_sq_sub (z w : ℂ) :

⇑complex.norm_sq (z - w) = ⇑complex.norm_sq z + ⇑complex.norm_sq w - 2 * (z * ⇑(star_ring_end ℂ) w).re

source

@[protected, instance]

noncomputable def complex.has_inv :

has_inv ℂ

Equations

complex.has_inv = {inv := λ (z : ℂ), ⇑(star_ring_end ℂ) z * ↑(⇑complex.norm_sq z)⁻¹}

source

theorem complex.inv_def (z : ℂ) :

z⁻¹ = ⇑(star_ring_end ℂ) z * ↑(⇑complex.norm_sq z)⁻¹

source

@[simp]

theorem complex.inv_re (z : ℂ) :

z⁻¹.re = z.re / ⇑complex.norm_sq z

source

@[simp]

theorem complex.inv_im (z : ℂ) :

z⁻¹.im = -z.im / ⇑complex.norm_sq z

source

@[simp, norm_cast]

theorem complex.of_real_inv (r : ℝ) :

↑r⁻¹ = (↑r)⁻¹

source

@[protected]

theorem complex.inv_zero :

0⁻¹ = 0

source

@[protected]

theorem complex.mul_inv_cancel {z : ℂ} (h : z ≠ 0) :

z * z⁻¹ = 1

source

@[protected, instance]

noncomputable def complex.field :

field ℂ

Equations

complex.field = {add := comm_ring.add complex.comm_ring, add_assoc := _, zero := comm_ring.zero complex.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul complex.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg complex.comm_ring, sub := comm_ring.sub complex.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul complex.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast complex.comm_ring, nat_cast := comm_ring.nat_cast complex.comm_ring, one := comm_ring.one complex.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul complex.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow complex.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv complex.has_inv, div := division_ring.div._default comm_ring.mul comm_ring.mul_assoc comm_ring.one comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' has_inv.inv, div_eq_mul_inv := complex.field._proof_1, zpow := division_ring.zpow._default comm_ring.mul comm_ring.mul_assoc comm_ring.one comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' has_inv.inv, zpow_zero' := complex.field._proof_2, zpow_succ' := complex.field._proof_3, zpow_neg' := complex.field._proof_4, exists_pair_ne := _, rat_cast := division_ring.rat_cast._default comm_ring.add comm_ring.add_assoc comm_ring.zero comm_ring.zero_add comm_ring.add_zero comm_ring.nsmul comm_ring.nsmul_zero' comm_ring.nsmul_succ' comm_ring.neg comm_ring.sub comm_ring.sub_eq_add_neg comm_ring.zsmul comm_ring.zsmul_zero' comm_ring.zsmul_succ' comm_ring.zsmul_neg' comm_ring.add_left_neg comm_ring.add_comm comm_ring.int_cast comm_ring.nat_cast comm_ring.one comm_ring.nat_cast_zero comm_ring.nat_cast_succ comm_ring.int_cast_of_nat comm_ring.int_cast_neg_succ_of_nat comm_ring.mul comm_ring.mul_assoc comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' comm_ring.left_distrib comm_ring.right_distrib has_inv.inv (division_ring.div._default comm_ring.mul comm_ring.mul_assoc comm_ring.one comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' has_inv.inv) complex.field._proof_5 (division_ring.zpow._default comm_ring.mul comm_ring.mul_assoc comm_ring.one comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' has_inv.inv) complex.field._proof_6 complex.field._proof_7 complex.field._proof_8, mul_inv_cancel := complex.mul_inv_cancel, inv_zero := complex.inv_zero, rat_cast_mk := complex.field._proof_9, qsmul := division_ring.qsmul._default (… comm_ring.zsmul_zero' comm_ring.zsmul_succ' comm_ring.zsmul_neg' comm_ring.add_left_neg comm_ring.add_comm comm_ring.int_cast comm_ring.nat_cast comm_ring.one comm_ring.nat_cast_zero comm_ring.nat_cast_succ comm_ring.int_cast_of_nat comm_ring.int_cast_neg_succ_of_nat comm_ring.mul comm_ring.mul_assoc comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' comm_ring.left_distrib comm_ring.right_distrib has_inv.inv (division_ring.div._default comm_ring.mul comm_ring.mul_assoc comm_ring.one comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' has_inv.inv) complex.field._proof_5 (division_ring.zpow._default comm_ring.mul comm_ring.mul_assoc comm_ring.one comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' has_inv.inv) complex.field._proof_6 complex.field._proof_7 complex.field._proof_8) comm_ring.add comm_ring.add_assoc comm_ring.zero comm_ring.zero_add comm_ring.add_zero comm_ring.nsmul comm_ring.nsmul_zero' comm_ring.nsmul_succ' comm_ring.neg comm_ring.sub comm_ring.sub_eq_add_neg comm_ring.zsmul comm_ring.zsmul_zero' comm_ring.zsmul_succ' comm_ring.zsmul_neg' comm_ring.add_left_neg comm_ring.add_comm comm_ring.int_cast comm_ring.nat_cast comm_ring.one comm_ring.nat_cast_zero comm_ring.nat_cast_succ comm_ring.int_cast_of_nat comm_ring.int_cast_neg_succ_of_nat comm_ring.mul comm_ring.mul_assoc comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' comm_ring.left_distrib comm_ring.right_distrib, qsmul_eq_mul' := complex.field._proof_10}

source

@[simp]

theorem complex.I_zpow_bit0 (n : ℤ) :

complex.I ^ bit0 n = (-1) ^ n

source

@[simp]

theorem complex.I_zpow_bit1 (n : ℤ) :

complex.I ^ bit1 n = (-1) ^ n * complex.I

source

theorem complex.div_re (z w : ℂ) :

(z / w).re = z.re * w.re / ⇑complex.norm_sq w + z.im * w.im / ⇑complex.norm_sq w

source

theorem complex.div_im (z w : ℂ) :

(z / w).im = z.im * w.re / ⇑complex.norm_sq w - z.re * w.im / ⇑complex.norm_sq w

source

theorem complex.conj_inv (x : ℂ) :

⇑(star_ring_end ℂ) x⁻¹ = (⇑(star_ring_end ℂ) x)⁻¹

source

@[simp, norm_cast]

theorem complex.of_real_div (r s : ℝ) :

↑(r / s) = ↑r / ↑s

source

@[simp, norm_cast]

theorem complex.of_real_zpow (r : ℝ) (n : ℤ) :

↑(r ^ n) = ↑r ^ n

source

@[simp]

theorem complex.div_I (z : ℂ) :

z / complex.I = -(z * complex.I)

source

@[simp]

theorem complex.inv_I :

complex.I ⁻¹ = -complex.I

source

@[simp]

theorem complex.norm_sq_inv (z : ℂ) :

⇑complex.norm_sq z⁻¹ = (⇑complex.norm_sq z)⁻¹

source

@[simp]

theorem complex.norm_sq_div (z w : ℂ) :

⇑complex.norm_sq (z / w) = ⇑complex.norm_sq z / ⇑complex.norm_sq w

source

@[simp, norm_cast]

theorem complex.of_real_nat_cast (n : ℕ) :

↑↑n = ↑n

source

@[simp, norm_cast]

theorem complex.nat_cast_re (n : ℕ) :

↑n.re = ↑n

source

@[simp, norm_cast]

theorem complex.nat_cast_im (n : ℕ) :

↑n.im = 0

source

@[simp, norm_cast]

theorem complex.of_real_int_cast (n : ℤ) :

↑↑n = ↑n

source

@[simp, norm_cast]

theorem complex.int_cast_re (n : ℤ) :

↑n.re = ↑n

source

@[simp, norm_cast]

theorem complex.int_cast_im (n : ℤ) :

↑n.im = 0

source

@[simp, norm_cast]

theorem complex.of_real_rat_cast (n : ℚ) :

↑↑n = ↑n

source

@[simp, norm_cast]

theorem complex.rat_cast_re (q : ℚ) :

↑q.re = ↑q

source

@[simp, norm_cast]

theorem complex.rat_cast_im (q : ℚ) :

↑q.im = 0

source

@[protected, instance]

def complex.char_zero_complex :

char_zero ℂ

source

theorem complex.re_eq_add_conj (z : ℂ) :

↑(z.re) = (z + ⇑(star_ring_end ℂ) z) / 2

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

source

theorem complex.im_eq_sub_conj (z : ℂ) :

↑(z.im) = (z - ⇑(star_ring_end ℂ) z) / (2 * complex.I)

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

source

theorem complex.abs_theory.abs_conj (z : ℂ) :

real.sqrt (⇑complex.norm_sq (⇑(star_ring_end ℂ) z)) = real.sqrt (⇑complex.norm_sq z)

source

noncomputable def complex.abs :

absolute_value ℂ ℝ

The complex absolute value function, defined as the square root of the norm squared.

Equations

complex.abs = {to_mul_hom := {to_fun := λ (x : ℂ), real.sqrt (⇑complex.norm_sq x), map_mul' := abs_mul}, nonneg' := abs_nonneg', eq_zero' := complex.abs._proof_1, add_le' := abs_add}

source

theorem complex.abs_def :

⇑complex.abs = λ (z : ℂ), real.sqrt (⇑complex.norm_sq z)

source

theorem complex.abs_apply {z : ℂ} :

⇑complex.abs z = real.sqrt (⇑complex.norm_sq z)

source

@[simp, norm_cast]

theorem complex.abs_of_real (r : ℝ) :

⇑complex.abs ↑r = |r|

source

theorem complex.abs_of_nonneg {r : ℝ} (h : 0 ≤ r) :

⇑complex.abs ↑r = r

source

theorem complex.abs_of_nat (n : ℕ) :

⇑complex.abs ↑n = ↑n

source

theorem complex.mul_self_abs (z : ℂ) :

⇑complex.abs z * ⇑complex.abs z = ⇑complex.norm_sq z

source

theorem complex.sq_abs (z : ℂ) :

⇑complex.abs z ^ 2 = ⇑complex.norm_sq z

source

@[simp]

theorem complex.sq_abs_sub_sq_re (z : ℂ) :

⇑complex.abs z ^ 2 - z.re ^ 2 = z.im ^ 2

source

@[simp]

theorem complex.sq_abs_sub_sq_im (z : ℂ) :

⇑complex.abs z ^ 2 - z.im ^ 2 = z.re ^ 2

source

@[simp]

theorem complex.abs_I :

⇑complex.abs complex.I = 1

source

@[simp]

theorem complex.abs_two :

⇑complex.abs 2 = 2

source

@[simp]

theorem complex.range_abs :

set.range ⇑complex.abs = set.Ici 0

source

@[simp]

theorem complex.abs_conj (z : ℂ) :

⇑complex.abs (⇑(star_ring_end ℂ) z) = ⇑complex.abs z

source

@[simp]

theorem complex.abs_prod {ι : Type u_1} (s : finset ι) (f : ι → ℂ) :

⇑complex.abs (s.prod f) = s.prod (λ (i : ι), ⇑complex.abs (f i))

source

@[simp]

theorem complex.abs_pow (z : ℂ) (n : ℕ) :

⇑complex.abs (z ^ n) = ⇑complex.abs z ^ n

source

@[simp]

theorem complex.abs_zpow (z : ℂ) (n : ℤ) :

⇑complex.abs (z ^ n) = ⇑complex.abs z ^ n

source

theorem complex.abs_re_le_abs (z : ℂ) :

|z.re | ≤ ⇑complex.abs z

source

theorem complex.abs_im_le_abs (z : ℂ) :

|z.im | ≤ ⇑complex.abs z

source

theorem complex.re_le_abs (z : ℂ) :

z.re ≤ ⇑complex.abs z

source

theorem complex.im_le_abs (z : ℂ) :

z.im ≤ ⇑complex.abs z

source

@[simp]

theorem complex.abs_re_lt_abs {z : ℂ} :

|z.re | < ⇑complex.abs z ↔ z.im ≠ 0

source

@[simp]

theorem complex.abs_im_lt_abs {z : ℂ} :

|z.im | < ⇑complex.abs z ↔ z.re ≠ 0

source

@[simp]

theorem complex.abs_abs (z : ℂ) :

|⇑complex.abs z| = ⇑complex.abs z

source

theorem complex.abs_le_abs_re_add_abs_im (z : ℂ) :

⇑complex.abs z ≤ |z.re | + |z.im |

source

theorem complex.abs_le_sqrt_two_mul_max (z : ℂ) :

⇑complex.abs z ≤ real.sqrt 2 * linear_order.max |z.re | |z.im |

source

theorem complex.abs_re_div_abs_le_one (z : ℂ) :

|z.re / ⇑complex.abs z| ≤ 1

source

theorem complex.abs_im_div_abs_le_one (z : ℂ) :

|z.im / ⇑complex.abs z| ≤ 1

source

@[simp, norm_cast]

theorem complex.abs_cast_nat (n : ℕ) :

⇑complex.abs ↑n = ↑n

source

@[simp, norm_cast]

theorem complex.int_cast_abs (n : ℤ) :

↑|n| = ⇑complex.abs ↑n

source

theorem complex.norm_sq_eq_abs (x : ℂ) :

⇑complex.norm_sq x = ⇑complex.abs x ^ 2

source

@[protected]

def complex.partial_order :

partial_order ℂ

We put a partial order on ℂ so that z ≤ w exactly if w - z is real and nonnegative. Complex numbers with different imaginary parts are incomparable.

Equations

complex.partial_order = {le := λ (z w : ℂ), z.re ≤ w.re ∧ z.im = w.im, lt := λ (z w : ℂ), z.re < w.re ∧ z.im = w.im, le_refl := complex.partial_order._proof_1, le_trans := complex.partial_order._proof_2, lt_iff_le_not_le := complex.partial_order._proof_3, le_antisymm := complex.partial_order._proof_4}

source

theorem complex.le_def {z w : ℂ} :

z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im

source

theorem complex.lt_def {z w : ℂ} :

z < w ↔ z.re < w.re ∧ z.im = w.im

source

@[simp, norm_cast]

theorem complex.real_le_real {x y : ℝ} :

↑x ≤ ↑y ↔ x ≤ y

source

@[simp, norm_cast]

theorem complex.real_lt_real {x y : ℝ} :

↑x < ↑y ↔ x < y

source

@[simp, norm_cast]

theorem complex.zero_le_real {x : ℝ} :

0 ≤ ↑x ↔ 0 ≤ x

source

@[simp, norm_cast]

theorem complex.zero_lt_real {x : ℝ} :

0 < ↑x ↔ 0 < x

source

theorem complex.not_le_iff {z w : ℂ} :

¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im

source

theorem complex.not_lt_iff {z w : ℂ} :

¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im

source

theorem complex.not_le_zero_iff {z : ℂ} :

¬z ≤ 0 ↔ 0 < z.re ∨ z.im ≠ 0

source

theorem complex.not_lt_zero_iff {z : ℂ} :

¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0

source

theorem complex.eq_re_of_real_le {r : ℝ} {z : ℂ} (hz : ↑r ≤ z) :

z = ↑(z.re)

source

@[protected]

def complex.strict_ordered_comm_ring :

strict_ordered_comm_ring ℂ

With z ≤ w iff w - z is real and nonnegative, ℂ is a strictly ordered ring.

Equations

complex.strict_ordered_comm_ring = {add := comm_ring.add complex.comm_ring, add_assoc := _, zero := comm_ring.zero complex.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul complex.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg complex.comm_ring, sub := comm_ring.sub complex.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul complex.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast complex.comm_ring, nat_cast := comm_ring.nat_cast complex.comm_ring, one := comm_ring.one complex.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul complex.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow complex.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := partial_order.le complex.partial_order, lt := partial_order.lt complex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := complex.strict_ordered_comm_ring._proof_1, exists_pair_ne := _, zero_le_one := complex.strict_ordered_comm_ring._proof_2, mul_pos := complex.strict_ordered_comm_ring._proof_3, mul_comm := _}

source

@[protected]

def complex.star_ordered_ring :

star_ordered_ring ℂ

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

Equations