Complex.I_mul_I
theorem Complex.I_mul_I : Complex.I * Complex.I = -1
This theorem states that the product of the complex imaginary unit with itself equals negative one. In terms of complex numbers, this can be written as `i * i = -1` where `i` stands for the imaginary unit and is represented as `Complex.I` in Lean 4. This is a fundamental property of the imaginary unit in the field of complex numbers.
More concisely: The square of the imaginary unit `Complex.I` in the complex numbers equals negative one, `i * i = -1`.
|
Complex.div_ofReal
theorem Complex.div_ofReal : ∀ (z : ℂ) (x : ℝ), z / ↑x = { re := z.re / x, im := z.im / x }
This theorem states that for any complex number `z` and real number `x`, the division of `z` by `x` (where `x` is treated as a complex number with zero imaginary part) equals a new complex number whose real part equals the real part of `z` divided by `x`, and whose imaginary part equals the imaginary part of `z` divided by `x`. In other words, dividing a complex number by a real number results in dividing both the real and imaginary parts of the complex number by the real number.
More concisely: For any complex number `z` and real number `x` (non-zero), the quotient of `z` by `x` is equal to the complex number with real part `(Re z) / x` and imaginary part `(Im z) / x`.
|
Mathlib.Data.Complex.Basic._auxLemma.9
theorem Mathlib.Data.Complex.Basic._auxLemma.9 : ∀ (n : ℤ) (r : ℝ), n • ↑r = ↑(n • r)
This theorem states that for any two real numbers `r` and `s`, the difference of their complex equivalents (denoted by `↑r` and `↑s`) is equal to the complex equivalent of their real difference (`r - s`). In mathematical terms, it asserts that for all real numbers r and s, (r - s) as a complex number is the same as the complex number r minus the complex number s.
More concisely: For all real numbers r and s, the complex numbers representing their real differences are equal: (r - s) = ↑r - ↑s.
|
Complex.conj_ofReal
theorem Complex.conj_ofReal : ∀ (r : ℝ), (starRingEnd ℂ) ↑r = ↑r
This theorem states that for any real number `r`, the conjugate of `r` when it is considered as a complex number (that is, converted from real to complex using `↑r`) is equal to `r` itself. In mathematical terms, if we denote complex conjugation by `starRingEnd ℂ`, this theorem says for every real number `r`, `(starRingEnd ℂ) ↑r = ↑r`. This is expected as the complex conjugate of a real number is the number itself, since it has no imaginary part to be negated.
More concisely: The real part of a complex number is equal to its complex conjugate for any real number. In Lean notation, `(starRingEnd ℂ) ↑r = ↑r` for all real numbers `r`.
|
Complex.ofReal_one
theorem Complex.ofReal_one : ↑1 = 1
This theorem states that the complex number representation of the real number 1 is equal to 1. In other words, when the real number 1 is converted to a complex number, it remains 1.
More concisely: The theorem asserts that the conversion of the real number 1 to a complex number results in the complex number 1. In mathematical notation: `1 = 1 : complex R`.
|
Complex.add_re
theorem Complex.add_re : ∀ (z w : ℂ), (z + w).re = z.re + w.re
This theorem states that for any two complex numbers `z` and `w`, the real part of the sum of `z` and `w` is equal to the sum of the real parts of `z` and `w`. In mathematical notation, this is saying that Re(z + w) = Re(z) + Re(w) for all complex numbers z and w. This is a fundamental property of complex numbers relating their addition operation to the real part operation.
More concisely: The real part of the sum of two complex numbers is equal to the sum of their real parts. (i.e. Re(z + w) = Re(z) + Re(w) for all complex numbers z and w)
|
Complex.ofReal_inj
theorem Complex.ofReal_inj : ∀ {z w : ℝ}, ↑z = ↑w ↔ z = w
This theorem states that for any two real numbers `z` and `w`, the complex number that `z` is converted to (`↑z`) is equal to the complex number that `w` is converted to (`↑w`) if and only if `z` is equal to `w`. In other words, the function that maps real numbers to complex numbers is injective, which means that different real numbers will be mapped to different complex numbers.
More concisely: The complex conversion function `↑` is injective on the real numbers, that is, for all real numbers `z` and `w`, `↑z = ↑w` implies `z = w`.
|
Mathlib.Data.Complex.Basic._auxLemma.1
theorem Mathlib.Data.Complex.Basic._auxLemma.1 : ∀ {z w : ℝ}, (↑z = ↑w) = (z = w)
This theorem in the Lean 4 Mathlib library states that for any two real numbers `z` and `w`, their respective complex number representations (denoted by `↑z` and `↑w`) are equal if and only if the original real numbers `z` and `w` themselves are equal. This equivalence is a fundamental property reflecting the relationship between the real and complex number systems.
More concisely: For any real numbers `z` and `w`, `↑z = ↑w` if and only if `z = w`.
|
Mathlib.Data.Complex.Basic._auxLemma.4
theorem Mathlib.Data.Complex.Basic._auxLemma.4 : ∀ (r s : ℝ), ↑r + ↑s = ↑(r + s)
This theorem, `Mathlib.Data.Complex.Basic._auxLemma.4`, states that for all real numbers `r` and `s`, the sum of their complex equivalents is equal to the complex equivalent of their sum. In mathematical notation, this is saying that for any real numbers `r` and `s`, the operation `↑r + ↑s = ↑(r + s)`, where `↑` denotes the conversion from real to complex numbers.
More concisely: For all real numbers r and s, converting their sum to complex numbers is equal to the sum of their individual complex conversions: ↑(r + s) = ↑r + ↑s.
|
Complex.im_eq_sub_conj
theorem Complex.im_eq_sub_conj : ∀ (z : ℂ), ↑z.im = (z - (starRingEnd ℂ) z) / (2 * Complex.I)
This theorem states that for any complex number `z`, the imaginary part of `z` is equal to the difference between `z` and its conjugate divided by `2i`. In other words, if we take a complex number, subtract its conjugate from it, and then divide the result by `2i`, we get the imaginary part of the initial complex number. This is a property of complex numbers and their conjugates.
More concisely: The imaginary part of a complex number `z` is equal to `(z - conjg z) / (2 * I)`, where `I` denotes the imaginary unit.
|
Complex.ofReal_neg
theorem Complex.ofReal_neg : ∀ (r : ℝ), ↑(-r) = -↑r
This theorem states that for every real number `r`, the complex embedding of the negation of `r` is equal to the negation of the complex embedding of `r`. In other words, it asserts that negation commutes with the process of embedding a real number into the complex numbers.
More concisely: For every real number `r`, the complex embeddings of `r` and its negation are complex conjugates of each other.
|
Complex.smul_re
theorem Complex.smul_re : ∀ {R : Type u_1} [inst : SMul R ℝ] (r : R) (z : ℂ), (r • z).re = r • z.re
This theorem states that for any type `R` that can be multiplied with real numbers, and any instance `r` of this type and a complex number `z`, the real part of the result of scaling `z` by `r` is equal to scaling the real part of `z` by `r`. In other words, scaling distributes over the operation of taking the real part in complex numbers.
More concisely: For any type `R` that supports real number multiplication, and `r` in `R` and complex number `z`, the real part of `r * z` equals the real part of `r * (re part z)`.
|
Complex.conj_eq_iff_re
theorem Complex.conj_eq_iff_re : ∀ {z : ℂ}, (starRingEnd ℂ) z = z ↔ ↑z.re = z
This theorem, named `Complex.conj_eq_iff_re`, states that for any given complex number `z`, the conjugate of `z` is equal to `z` if and only if `z` is equal to its real part. Here, `starRingEnd ℂ` represents the conjugate of a complex number, and `↑z.re` represents the real part of `z`. Consequently, this theorem essentially says that a complex number is equal to its conjugate (meaning that its imaginary part is zero) if and only if it is a real number.
More concisely: A complex number is equal to its conjugate if and only if it is a real number. (equivalently, a complex number z has zero imaginary part if and only if z = ↑z.re)
|
Complex.normSq_eq_zero
theorem Complex.normSq_eq_zero : ∀ {z : ℂ}, Complex.normSq z = 0 ↔ z = 0
This theorem states that for any complex number `z`, the norm-squared function `Complex.normSq z` equals zero if and only if `z` itself is zero. The norm-squared function for a complex number is defined as the square of the real part plus the square of the imaginary part. Hence, both parts must be zero for the norm-squared to be zero, which implies that the complex number itself is zero.
More concisely: The theorem asserts that the norm-squared of a complex number equals zero if and only if the complex number is the zero.
|
Complex.real_smul
theorem Complex.real_smul : ∀ {x : ℝ} {z : ℂ}, x • z = ↑x * z
This theorem states that for every real number `x` and every complex number `z`, the action of scaling `z` by `x` (denoted `x • z`) is equal to the product of `x` and `z` (denoted `↑x * z`). Here, `↑x` represents the embedding of the real number `x` in the complex numbers. Therefore, this theorem links scalar multiplication in the field of complex numbers with multiplication by a real number.
More concisely: For every real number x and complex number z, x • z = ↑x * z. (Scalar multiplication in the complex numbers equals multiplication by a real number.)
|
Complex.normSq_nonneg
theorem Complex.normSq_nonneg : ∀ (z : ℂ), 0 ≤ Complex.normSq z
This theorem states that for all complex numbers `z`, the square of the norm of `z` (denoted by `Complex.normSq z`) is always greater than or equal to zero. In mathematical terms, it asserts that ∀ z ∈ ℂ, 0 ≤ ||z||², where ||z||² is the squared norm of `z`, calculated as the sum of the squares of the real and imaginary parts of `z`.
More concisely: For all complex numbers z, the square of its norm is non-negative: 0 ≤ ||z||², where ||z||² is the sum of the squares of its real and imaginary parts.
|
Complex.ofReal_ofNat
theorem Complex.ofReal_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
This theorem, named `Complex.ofReal_ofNat`, states that for all natural numbers `n` with a given instance `inst` asserting that `n` is at least two, the coercion of `OfNat.ofNat n` to a complex number is equal to `OfNat.ofNat n` itself. This essentially means that the behavior of `OfNat.ofNat` function remains consistent when the numeric literal `n` of type `α` is considered as a complex number, given that `n` is a natural number greater than or equal to two. The `OfNat.ofNat` function is inserted automatically by the Lean parser when a numeric literal like `n : α` is written.
More concisely: For all natural numbers `n` greater than or equal to 2, `OfNat.ofNat n` is equal to its complex coercion.
|
Mathlib.Data.Complex.Basic._auxLemma.8
theorem Mathlib.Data.Complex.Basic._auxLemma.8 : ∀ (n : ℕ) (r : ℝ), n • ↑r = ↑(n • r)
This theorem states that for any complex number 'z', the norm squared of 'z' (denoted as Complex.normSq z), is greater than zero if and only if 'z' is not equal to zero. In other words, the norm squared of a complex number is positive if the complex number is non-zero.
More concisely: The theorem asserts that the square of the complex norm is positive for non-zero complex numbers.
|
Complex.ofReal_zero
theorem Complex.ofReal_zero : ↑0 = 0
This theorem states that the complex number representation of a real zero is equal to zero. In other words, when you convert the real number zero to a complex number, the result is still zero.
More concisely: The theorem asserts that the conversion of the real number 0 to a complex number results in the complex number 0.
|
Complex.ofReal_im
theorem Complex.ofReal_im : ∀ (r : ℝ), (↑r).im = 0
This theorem states that the imaginary part of any real number `r` expressed as a complex number is always zero. In other words, when a real number is considered as a complex number (by being cast to a complex number via `(↑r)`), its imaginary component is always `0`. This theorem stands true for every real number `r`.
More concisely: The real part of a real number, when considered as a complex number, is always equal to its real part and its imaginary part is always zero. (Or equivalently, the imaginary part of a real number as a complex number is always 0.)
|
Complex.ext_iff
theorem Complex.ext_iff : ∀ {z w : ℂ}, z = w ↔ z.re = w.re ∧ z.im = w.im
This theorem states that for any two complex numbers `z` and `w`, `z` is equal to `w` if and only if the real part of `z` (`z.re`) is equal to the real part of `w` (`w.re`) and the imaginary part of `z` (`z.im`) is equal to the imaginary part of `w` (`w.im`). In other words, two complex numbers are identical when both their real and imaginary components match.
More concisely: Two complex numbers are equal if and only if their real and imaginary parts are equal respectively.
|
Complex.neg_re
theorem Complex.neg_re : ∀ (z : ℂ), (-z).re = -z.re
This theorem states that the real part of the negation of a complex number is equal to the negation of the real part of the original complex number. In other words, if you have a complex number `z`, and you negate this number to get `-z`, then the real part of `-z` (`(-z).re`) is identical to the negative of the real part of `z` (`-z.re`).
More concisely: The real part of the negation of a complex number equals the negative of the real part of the original complex number. In mathematical notation, this can be expressed as `(-\ complex.re z).equiv (- z.re)`.
|
Complex.ofReal_re
theorem Complex.ofReal_re : ∀ (r : ℝ), (↑r).re = r
This theorem states that for any real number `r`, the real part of the complex number obtained by coercing `r` to a complex number is equal to `r` itself. In other words, the real component of a complex number created from a real number is just the original real number. The `.re` function in this context is used to extract the real part of a complex number.
More concisely: For any real number `r`, the real part of the complex number obtained by coercing `r` is equal to `r` itself. (In Lean: `(real.coerce r).re = r`)
|
Complex.ofReal_pow
theorem Complex.ofReal_pow : ∀ (r : ℝ) (n : ℕ), ↑(r ^ n) = ↑r ^ n
This theorem states that for any real number `r` and any natural number `n`, the complex number obtained by taking `r` to the power of `n` and then casting to a complex number is equal to the complex number obtained by first casting `r` to a complex number and then taking it to the power of `n`. That is, the process of exponentiation and the process of casting real numbers to complex numbers commute with each other. In mathematical notation, this can be written as `(r ^ n) = r ^ n` for all real numbers `r` and all natural numbers `n`, where `^` denotes exponentiation and `(·)` denotes the complex conjugate.
More concisely: For all real numbers `r` and natural numbers `n`, the result of raising `r` to the power `n` as a complex number is equal to the result of first casting `r` to a complex number and then raising it to the power `n`. In other words, the operations of exponentiation and casting real numbers to complex numbers commute.
|
Complex.ofReal_sub
theorem Complex.ofReal_sub : ∀ (r s : ℝ), ↑(r - s) = ↑r - ↑s
This theorem states that for all real numbers `r` and `s`, the complex representation of the difference between `r` and `s` is equal to the difference of the complex representations of `r` and `s`. In other words, the operation of subtraction is preserved under the function that maps real numbers to their complex counterparts.
More concisely: For all real numbers r and s, (r : ℝ) → ℂ) (s : ℝ) := ⇑(-) r s = ((-): ℝ → ℝ → ℝ) r s : ℂ, where (-) is real number subtraction and (-) is complex number subtraction.
|
Complex.ofReal_mul
theorem Complex.ofReal_mul : ∀ (r s : ℝ), ↑(r * s) = ↑r * ↑s
This theorem states that for any two real numbers `r` and `s`, the complex representation of their product is equal to the product of their complex representations. In other words, if you multiply two real numbers and then convert the result to a complex number, you'll get the same result as if you converted the two real numbers to complex numbers first and then multiplied them together. This is written in mathematical notation as: ∀ (r s : ℝ), ↑(r * s) = ↑r * ↑s.
More concisely: For all real numbers r and s, the complex number representation of their product equals the product of their individual complex number representations. (i.e., ∀ (r s : ℝ), ↑(r * s) = ↑r * ↑s)
|
Complex.im_ofReal_mul
theorem Complex.im_ofReal_mul : ∀ (r : ℝ) (z : ℂ), (↑r * z).im = r * z.im
This theorem, `Complex.im_ofReal_mul`, states that for all real numbers `r` and complex numbers `z`, the imaginary part of the product of `r` (converted into a complex number) and `z` is equal to `r` multiplied by the imaginary part of `z`. In mathematical terms, it expresses that Im(rz) = r * Im(z), where Im denotes the imaginary part of a complex number.
More concisely: The imaginary part of the product of a real number and a complex number is equal to the real number times the imaginary part of the complex number.
|
Mathlib.Data.Complex.Basic._auxLemma.12
theorem Mathlib.Data.Complex.Basic._auxLemma.12 : ∀ (r : ℝ) (n : ℕ), ↑r ^ n = ↑(r ^ n)
This theorem states that for all natural numbers `n` and for all real numbers `r`, the scalar multiplication of `n` and the complex number form of `r` is equal to the complex number form of the scalar multiplication of `n` and `r`. In mathematical symbols, for all n in ℕ and r in ℝ, n * complex(r) = complex(n * r).
More concisely: For all natural numbers n and real numbers r, the scalar multiplication of n with the complex number ir is equal to the complex number obtained by scaling ir by n.
|
Complex.zero_re
theorem Complex.zero_re : Complex.re 0 = 0
This theorem states that the real part of the complex number zero is zero. In the field of complex numbers, each number is represented as a combination of a real part and an imaginary part. This theorem confirms that for the complex number zero, the real part is also zero.
More concisely: The real part of the complex number zero is equal to zero.
|
Complex.re_eq_add_conj
theorem Complex.re_eq_add_conj : ∀ (z : ℂ), ↑z.re = (z + (starRingEnd ℂ) z) / 2
This theorem states that for any complex number `z`, the real part of the complex number, denoted as `z.re`, is equal to the sum of the complex number and its conjugate, divided by `2`. The conjugate of the complex number is computed using the `starRingEnd` function in the Complex domain. In mathematical terms expressed using LaTeX, if `z` is a complex number, the real part of `z` is `(z + \overline{z}) / 2`, where `\overline{z}` denotes the complex conjugate of `z`.
More concisely: The real part of a complex number `z` is equal to the average of `z` and its conjugate.
|
Complex.ofReal_div
theorem Complex.ofReal_div : ∀ (r s : ℝ), ↑(r / s) = ↑r / ↑s
This theorem states that for any two real numbers `r` and `s`, the complex representation (or 'embedding') of the division of `r` by `s` is equal to the division of the complex representations of `r` and `s`. In mathematical terms, it means for all real numbers `r` and `s`, we have `(r / s) = r / s` in the complex number space, where the left side is the real number division operation and the right side is the complex number division operation.
More concisely: For all real numbers r and s, the complex representation of r divided by s equals the complex division of the complex representations of r and s.
|
Complex.one_re
theorem Complex.one_re : Complex.re 1 = 1
This theorem states that the real part of the complex number 1 is 1. In the context of complex numbers, each number is composed of a real and an imaginary part. In this case, the number being considered is 1 which is purely real, hence its real part is 1.
More concisely: The real part of the complex number 1 is equal to 1.
|
Complex.inv_re
theorem Complex.inv_re : ∀ (z : ℂ), z⁻¹.re = z.re / Complex.normSq z
The theorem `Complex.inv_re` states that for any complex number `z`, the real part of the reciprocal of `z` is equal to the real part of `z` divided by the square of the norm of `z`. In mathematical terms, if `z` is a complex number, then the real part of `1/z` is equal to `Re(z) / ||z||^2`.
More concisely: The real part of the complex conjugate of the reciprocal of a complex number `z` is equal to the reciprocal of the square of its norm: `Real part(conjg z!*1) = 1 / ||z||^2`.
|
Complex.equivRealProd_symm_apply
theorem Complex.equivRealProd_symm_apply : ∀ (p : ℝ × ℝ), Complex.equivRealProd.symm p = ↑p.1 + ↑p.2 * Complex.I := by
sorry
This theorem states that for every pair of real numbers `p`, the inverse function of the equivalence between the complex numbers and the real numbers product, applied to `p`, equals the first element of `p` (treated as a complex number) plus the second element of `p` (also treated as a complex number) multiplied by the imaginary unit. In mathematical terms, for all `(a, b) ∈ ℝ × ℝ`, this function maps `(a, b)` to `a + b * i`, where `i` is the imaginary unit.
More concisely: For every real number pair `(a, b)`, the function mapping `(a, b)` to `a + b*i` (where `i` is the imaginary unit) holds true in the equivalence between complex and real numbers.
|
Complex.inv_im
theorem Complex.inv_im : ∀ (z : ℂ), z⁻¹.im = -z.im / Complex.normSq z
The theorem `Complex.inv_im` states that for any complex number `z`, the imaginary part of the inverse of `z` is equal to the negation of the imaginary part of `z` divided by the square of the norm of `z`. Here, the norm of a complex number `z` is defined as the sum of the squares of its real and imaginary parts, and the inverse of `z` is the complex number which multiplied by `z` gives the number 1.
More concisely: The imaginary part of the complex number inverse to `z` is equal to -(imaginary part of `z`) / (norm of `z`)² for any complex number `z`.
|
Complex.conj_eq_iff_im
theorem Complex.conj_eq_iff_im : ∀ {z : ℂ}, (starRingEnd ℂ) z = z ↔ z.im = 0
This theorem states that for any complex number 'z', the conjugate of 'z' is equal to 'z' if and only if the imaginary part of 'z' is zero. In other words, a complex number is equal to its own conjugate only when it is a real number (since real numbers have zero imaginary parts).
More concisely: A complex number is equal to its conjugate if and only if it is a real number (equivalent to having an imaginary part of 0).
|
Complex.ofReal_injective
theorem Complex.ofReal_injective : Function.Injective Complex.ofReal'
The theorem `Complex.ofReal_injective` states that the function `Complex.ofReal'`, which maps a real number to a complex number (by associating the real number to the real part of the complex number and setting the imaginary part to zero), is injective. In other words, if two real numbers are mapped to the same complex number by this function, then those two real numbers must have been the same. This theorem ensures that no information is lost when real numbers are embedded into the complex numbers in this way.
More concisely: The theorem `Complex.ofReal_injective` asserts that the function `Complex.ofReal'` maps distinct real numbers to distinct complex numbers.
|
Complex.conj_I
theorem Complex.conj_I : (starRingEnd ℂ) Complex.I = -Complex.I
This theorem states that the complex conjugate of the imaginary unit in complex numbers, denoted as `Complex.I`, is equal to the negative of the imaginary unit. In mathematical terms, the complex conjugate of `i` (i.e., the imaginary unit) is `-i`. This is represented in Lean 4 as `(starRingEnd ℂ) Complex.I = -Complex.I`.
More concisely: The complex conjugate of `Complex.I` equals `-Complex.I` in the complex number field.
|
Complex.ofReal_eq_zero
theorem Complex.ofReal_eq_zero : ∀ {z : ℝ}, ↑z = 0 ↔ z = 0
This theorem, `Complex.ofReal_eq_zero`, states that for all real numbers 'z', the complex number representation of 'z' (denoted as `↑z`) is equal to zero if and only if 'z' itself is zero. In other words, a real number can be represented as zero in the complex number plane only when it is zero in the real number line.
More concisely: The complex representation `↑z` of a real number `z` equals zero if and only if `z` itself is zero.
|
Complex.I_ne_zero
theorem Complex.I_ne_zero : Complex.I ≠ 0
This theorem states that the imaginary unit (often denoted as 'i' in mathematical literature) in the field of complex numbers is not equal to zero. In other words, the complex number whose real part is zero and imaginary part is one, denoted as `Complex.I` in Lean 4, is not the same as the number zero.
More concisely: The imaginary unit `Complex.I` in the field of complex numbers is distinct from the zero element.
|
Complex.re_add_im
theorem Complex.re_add_im : ∀ (z : ℂ), ↑z.re + ↑z.im * Complex.I = z
The theorem `Complex.re_add_im` states that for every complex number `z`, the real part of `z` plus the imaginary part of `z` times the imaginary unit equals `z` itself. In mathematical notation, this would be expressed as: for all complex numbers `z`, `Re(z) + Im(z) * i = z`. This theorem is a formalization of the standard presentation of a complex number in terms of its real and imaginary parts.
More concisely: For every complex number z, Re(z) + Im(z) * i = z.
|
Complex.ofReal_ne_zero
theorem Complex.ofReal_ne_zero : ∀ {z : ℝ}, ↑z ≠ 0 ↔ z ≠ 0
This theorem states that for any real number `z`, the complex representation of `z` (denoted by `↑z`) is not equal to zero if and only if `z` is not equal to zero. In other words, a real number and its complex representation are simultaneously non-zero.
More concisely: For any real number `z`, `↑z ≠ 0` if and only if `z ≠ 0`.
|
Mathlib.Data.Complex.Basic._auxLemma.11
theorem Mathlib.Data.Complex.Basic._auxLemma.11 : ∀ (r s : ℝ), ↑r - ↑s = ↑(r - s)
This theorem states that for every real number `r`, the reciprocal of the complex embedding of `r` is equal to the complex embedding of the reciprocal of `r`. In other words, taking the reciprocal before or after embedding a real number into the complex numbers yields the same result.
More concisely: For all real numbers r, the complex embeddings of r and its reciprocal are equal. In Lean notation: `complex_abs r = complex_abs (1 / r)`.
|
Complex.re_ofReal_mul
theorem Complex.re_ofReal_mul : ∀ (r : ℝ) (z : ℂ), (↑r * z).re = r * z.re
This theorem states that for any real number `r` and any complex number `z`, the real part of the product of `r` (converted to a complex number) and `z` is equal to `r` multiplied by the real part of `z`. In terms of mathematical notation, this would be represented as Re(rz) = rRe(z) where `Re` represents the real part of a complex number.
More concisely: The real part of the product of a real number and a complex number is equal to the real number times the real part of the complex number. In Lean notation, Re(r * z) = r * Re(z).
|
Complex.add_im
theorem Complex.add_im : ∀ (z w : ℂ), (z + w).im = z.im + w.im
This theorem states that for any two complex numbers `z` and `w`, the imaginary part of the sum of `z` and `w` is equal to the sum of the imaginary parts of `z` and `w`. In other words, if `ℂ` denotes the set of complex numbers, then for every `z, w ∈ ℂ`, the imaginary part of `(z + w)` is the same as the sum of the imaginary parts of `z` and `w`. This is the algebraic property of complex numbers related to the addition operation on the imaginary parts.
More concisely: The theorem asserts that for all complex numbers `z` and `w`, the imaginary part of their sum equals the sum of their imaginary parts. (Imag(z + w) = Imag(z) + Imag(w)).
|
Complex.normSq_pos
theorem Complex.normSq_pos : ∀ {z : ℂ}, 0 < Complex.normSq z ↔ z ≠ 0
The theorem `Complex.normSq_pos` states that for any complex number `z`, the norm squared function `Complex.normSq z` is positive if and only if `z` is not equal to zero. This theorem encapsulates the result that a complex number's square of the norm (or magnitude) is strictly greater than zero if the complex number itself is not zero.
More concisely: For any complex number z, the square of its norm is positive if and only if z is non-zero.
|
Complex.smul_im
theorem Complex.smul_im : ∀ {R : Type u_1} [inst : SMul R ℝ] (r : R) (z : ℂ), (r • z).im = r • z.im
This theorem states that for any real scalar `r` and any complex number `z`, the imaginary part of the scaled complex number (`r • z`) is equal to the scaled imaginary part of the complex number (`r • z.im`). In other words, scalar multiplication distributes over the imaginary part of a complex number.
More concisely: For any real scalar r and complex number z, the imaginary parts of r * z and r * (z.im) are equal.
|
Complex.ofReal_add
theorem Complex.ofReal_add : ∀ (r s : ℝ), ↑(r + s) = ↑r + ↑s
This theorem, `Complex.ofReal_add`, states that for any two real numbers `r` and `s`, the complex representation of the sum of `r` and `s` is equal to the sum of the complex representation of `r` and the complex representation of `s`. In other words, the process of converting a real number to a complex number commutes with the operation of addition.
More concisely: For any real numbers r and s, Complex.ofReal r + Complex.ofReal s = Complex.ofReal (r + s).
|
Complex.normSq_ofReal
theorem Complex.normSq_ofReal : ∀ (r : ℝ), Complex.normSq ↑r = r * r
This theorem, `Complex.normSq_ofReal`, states that for every real number `r`, the square of the complex norm (or magnitude) of the complex number `r` (obtained by considering `r` as a complex number with zero imaginary part) is equal to `r * r`. In mathematical notation, for all real numbers `r`, the square of the norm of `r` as a complex number is the square of `r` itself.
More concisely: For every real number r, the complex norm of r squared equals r squared.
|
Complex.ext
theorem Complex.ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w
This theorem states that for any two complex numbers `z` and `w`, if their real parts (`z.re` and `w.re`) are equal and their imaginary parts (`z.im` and `w.im`) are also equal, then `z` and `w` must be the same complex number. Essentially, it confirms the intuition that two complex numbers are identical if and only if both their real and imaginary components are identical.
More concisely: If two complex numbers `z` and `w` have equal real and imaginary parts, i.e., `z.re = w.re` and `z.im = w.im`, then `z = w`.
|
Complex.I_sq
theorem Complex.I_sq : Complex.I ^ 2 = -1
This theorem states that the square of the imaginary unit in complex numbers equals negative one. In mathematical terms, it corresponds to the well-known identity i² = -1, where i is the imaginary unit, a fundamental concept in complex number theory.
More concisely: The square of the imaginary unit i in complex numbers equals negative one. (i.e., i² = -1)
|
Complex.normSq_neg
theorem Complex.normSq_neg : ∀ (z : ℂ), Complex.normSq (-z) = Complex.normSq z
The theorem `Complex.normSq_neg` states that for every complex number `z`, the norm squared of the negation of `z` is equal to the norm squared of `z` itself. In mathematical terms, if we denote the norm squared function as `||.||²`, this property can be written as `||-z||² = ||z||²` for all complex numbers `z`. This implies that negating a complex number does not change its norm squared.
More concisely: The norm squared of the negation of a complex number equals the norm squared of the number itself. That is, `||-z||² = ||z||²` for all complex numbers `z`.
|
Mathlib.Data.Complex.Basic._auxLemma.2
theorem Mathlib.Data.Complex.Basic._auxLemma.2 : ∀ {z : ℝ}, (↑z = 0) = (z = 0)
This theorem states that for every real number `z`, the complex equivalent of `z` (denoted as `↑z`) is equal to zero if and only if `z` itself is equal to zero. In other words, a real number and its complex counterpart are both zero at the same time, and no other situation will make them equal to zero simultaneously.
More concisely: For every real number `z`, `↑z = 0` if and only if `z = 0`.
|
Complex.inv_def
theorem Complex.inv_def : ∀ (z : ℂ), z⁻¹ = (starRingEnd ℂ) z * ↑(Complex.normSq z)⁻¹
This theorem states that for any complex number `z`, the multiplicative inverse of `z` (denoted `z⁻¹`) is equal to the product of the conjugate of `z` (denoted `(starRingEnd ℂ) z`), and the reciprocal of the norm squared of `z` (denoted `↑(Complex.normSq z)⁻¹`). Here, the norm squared of a complex number is the sum of the square of the real part and the square of the imaginary part of the complex number, and the conjugate of a complex number is obtained by changing the sign of its imaginary part.
More concisely: For any complex number `z`, its multiplicative inverse is equal to the product of the conjugate of `z` and the reciprocal of the square of its norm, i.e., `z⁻¹ = (starRingEnd ℂ z) / (↑(Complex.normSq z)`) where the norm of `z` is the square root of the sum of the squares of its real and imaginary parts.
|
Complex.ofReal_inv
theorem Complex.ofReal_inv : ∀ (r : ℝ), ↑r⁻¹ = (↑r)⁻¹
This theorem states that for all real numbers `r`, the reciprocal of the complex number corresponding to `r` is equal to the complex number corresponding to the reciprocal of `r`. In other words, taking the reciprocal before or after the real-to-complex conversion gives the same result. Here, `↑r` denotes the complex number corresponding to the real number `r`.
More concisely: For all real numbers `r`, the complex numbers `(↑r)^-1` and `↑(r^-1)` are equal.
|
Complex.normSq_apply
theorem Complex.normSq_apply : ∀ (z : ℂ), Complex.normSq z = z.re * z.re + z.im * z.im
This theorem, `Complex.normSq_apply`, states that for all complex numbers `z`, the application of the function `Complex.normSq` to `z` is equal to the sum of the square of the real part of `z` and the square of the imaginary part of `z`. In mathematical terms, for any complex number `z`, `Complex.normSq z = Re(z)^2 + Im(z)^2`, where `Re(z)` and `Im(z)` denote the real and imaginary parts of `z`, respectively.
More concisely: The theorem asserts that for any complex number `z`, the square of its norm equals the sum of the squares of its real and imaginary parts: `Complex.normSq z = Re(z)² + Im(z)²`.
|