Complex.algHom_ext
theorem Complex.algHom_ext :
∀ {A : Type u_3} [inst : Semiring A] [inst_1 : Algebra ℝ A] ⦃f g : ℂ →ₐ[ℝ] A⦄, f Complex.I = g Complex.I → f = g
This theorem states that for any type `A` which has a semiring and an algebra structure over the real numbers, two algebra homomorphisms from the complex numbers to `A` are considered to be equal if they agree on the value of `Complex.I`, the imaginary unit. In other words, if two algebra homomorphisms from the complex numbers to `A` map the imaginary unit to the same element in `A`, then these two homomorphisms are indeed the same.
More concisely: For any type `A` equipped with a semiring and algebra structure over the real numbers, two algebra homomorphisms from the complex numbers to `A` are equal if they map the imaginary unit `I` to the same element in `A`.
|
Complex.toMatrix_conjAe
theorem Complex.toMatrix_conjAe :
(LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) Complex.conjAe.toLinearMap =
Matrix.of ![![1, 0], ![0, -1]]
This theorem specifies the matrix representation of the complex conjugation function, `conjAe`, in the basis given by `1` and `I` for the complex numbers as a real vector space. Specifically, it states that the matrix representation of the complex conjugation linear map is the 2x2 matrix with entries `1` and `-1` on the diagonal and `0` elsewhere. This corresponds to the traditional matrix representation of complex conjugation in the standard basis, where the real part is left unchanged, and the imaginary part is negated.
More concisely: The matrix representation of the complex conjugation linear map with respect to the basis {1, I} for the complex numbers as a real vector space is the 2x2 matrix with diagonal entries 1 and -1.
|
Complex.liftAux_apply_I
theorem Complex.liftAux_apply_I :
∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] (I' : A) (hI' : I' * I' = -1),
(Complex.liftAux I' hI') Complex.I = I'
The theorem `Complex.liftAux_apply_I` states that for any real algebra type `A` that has both a ring structure and an algebra structure, given any element `I'` in `A` such that the square of `I'` equals `-1`, the application of the `liftAux` function on `I'` and the imaginary unit of complex numbers equals `I'`. In other words, the function `Complex.liftAux` maps the imaginary unit of complex numbers to an element which squares to `-1` in any real algebraic structure.
More concisely: For any real algebra type `A` with ring and algebra structures, and any element `I'` in `A` satisfying `I'` ^ 2 = -1, Complex.liftAux `I'` equals `I'`.
|
Complex.nonempty_linearEquiv_real
theorem Complex.nonempty_linearEquiv_real : Nonempty (ℂ ≃ₗ[ℚ] ℝ)
This theorem states that the complex numbers (`ℂ`) and the real numbers (`ℝ`) are isomorphic as vector spaces over the rational numbers (`ℚ`). In other words, there exists a bijective linear transformation between `ℂ` and `ℝ` that preserves vector space operations. Equivalently, the complex numbers and real numbers form isomorphic additive groups.
More concisely: The complex numbers and real numbers are isomorphic as vector spaces over the rational numbers.
|
realPart_add_I_smul_imaginaryPart
theorem realPart_add_I_smul_imaginaryPart :
∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
(a : A), ↑(realPart a) + Complex.I • ↑(imaginaryPart a) = a
The theorem `realPart_add_I_smul_imaginaryPart` states that for any element 'a' from a star module over the complex numbers (ℂ), the element 'a' can be expressed as the linear combination of its self adjoint real part and the imaginary part scaled by the imaginary unit (ℜ a + Complex.I • ℑ a = a). This is commonly known as the standard decomposition of a complex number or an element from a star module over complex numbers.
More concisely: For any complex number a, a can be expressed as the sum of its real part and the imaginary part multiplied by the imaginary unit (a = ℜ a + I * ℑ a).
|
realPart_apply_coe
theorem realPart_apply_coe :
∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
(a : A), ↑(realPart a) = 2⁻¹ • (a + star a)
This theorem, `realPart_apply_coe`, states that for any element `a` from a Star Module `A` over the complex numbers (ℂ), where `A` is also an additive commutative group and a Star Additive Monoid, the real part of `a` (denoted as `ℜ a`) when casted, equals half of the sum of `a` and its conjugate (`star a`). In other words, the real part of `a` in such context is computed as one-half times the sum of `a` and its complex conjugate.
More concisely: For any complex number `a` in a star module `A` over ℂ that is an additive commutative group and a star additive monoid, the real part `ℜ a` is equal to (1/2) * (a + conjugate `a`).
|
Complex.real_algHom_eq_id_or_conj
theorem Complex.real_algHom_eq_id_or_conj : ∀ (f : ℂ →ₐ[ℝ] ℂ), f = AlgHom.id ℝ ℂ ∨ f = ↑Complex.conjAe
This theorem states that any real algebra homomorphism from the complex numbers to itself is either the identity function or the complex conjugation. That is, if we have a function `f` that is a homomorphism from the algebra of complex numbers over the real numbers back to itself, then that function must be either the identity function (mapping every complex number to itself), or the complex conjugation function (mapping every complex number to its complex conjugate).
More concisely: Any real algebra homomorphism from the complex numbers to themselves is either the identity function or complex conjugation.
|
Complex.finrank_real_complex_fact
theorem Complex.finrank_real_complex_fact : Fact (FiniteDimensional.finrank ℝ ℂ = 2)
This theorem states a mathematical fact: the finite dimensional rank of the complex numbers (`ℂ`) as a vector space over the real numbers (`ℝ`) is 2. In other words, it asserts that the dimension of the complex numbers when viewed as a vector space over the real numbers is precisely 2. This fact is commonly used, for example, in defining the circle in the complex plane.
More concisely: The complex numbers, viewed as a vector space over the real numbers, have dimension 2.
|
Complex.finrank_real_complex
theorem Complex.finrank_real_complex : FiniteDimensional.finrank ℝ ℂ = 2
This theorem states that the rank of the complex numbers when considered as a module over the real numbers is equal to 2. In other words, it is asserting that the complex numbers form a two-dimensional vector space over the real numbers.
More concisely: The complex numbers form a 2-dimensional vector space over the real numbers.
|
imaginaryPart_apply_coe
theorem imaginaryPart_apply_coe :
∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
(a : A), ↑(imaginaryPart a) = -Complex.I • 2⁻¹ • (a - star a)
This theorem states that for any type `A` that is a commutative additive group and a module over the complex numbers, and additionally has the structure of a star-additive monoid and a star module over the complex numbers, the imaginary part of an element `a` of type `A`, when promoted to the complex number, is equal to negative of the imaginary unit `Complex.I` scaled by one half, and then scaled by the difference between `a` and its star conjugate. In mathematical notation, this would be $\Im(a) = -i \cdot \frac{1}{2} \cdot (a - a^*)$ where $\Im$ denotes the imaginary part, $i$ is the imaginary unit, and $*$ denotes the star operation.
More concisely: The imaginary part of an element in a complex-valued commutative additive group with star-additive monoid and star module structures is equal to negative half of the imaginary unit times the difference between the element and its star conjugate.
|
AlgHom.map_coe_real_complex
theorem AlgHom.map_coe_real_complex :
∀ {A : Type u_3} [inst : Semiring A] [inst_1 : Algebra ℝ A] (f : ℂ →ₐ[ℝ] A) (x : ℝ), f ↑x = (algebraMap ℝ A) x := by
sorry
The theorem `AlgHom.map_coe_real_complex` states that for any semiring `A` with an algebra structure over the real numbers (`ℝ`), any complex algebra homomorphism (`ℂ →ₐ[ℝ] A`) `f`, and any real number `x`, the value of `f` when applied to the complex embedding of `x` (`f ↑x`) is equal to the application of the algebra map from the real numbers to `A` on `x` (`(algebraMap ℝ A) x`). This theorem is required since `Complex.coe_algebraMap` changes the simplification-normal form away from `AlgHom.commutes`.
More concisely: For any semiring `A` with an algebra structure over the real numbers, any complex algebra homomorphism `f : ℂ →ₐ[ℝ] A` satisfies `f (Complex.embedding ℝ x) = algebraMap ℝ A x` for all real numbers `x`.
|
IsSelfAdjoint.coe_realPart
theorem IsSelfAdjoint.coe_realPart :
∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
{x : A}, IsSelfAdjoint x → ↑(realPart x) = x
The theorem `IsSelfAdjoint.coe_realPart` states that for any type `A` that forms an additive commutative group, is a complex module, has a star add monoid structure, and is a star module over complex numbers, if an element `x` of `A` is self-adjoint, then the real part of `x` (considered as an element of the self-adjoint part of `A`) is equal to `x` itself. In other words, for a self-adjoint element in such a structure, the real part operation simply returns the element itself.
More concisely: If `A` is a complex module, additive commutative group, has a star add monoid structure, and is a star module over complex numbers, then a self-adjoint element `x` in `A` equals its real part.
|