Revision #1702 → #2259 · back to history
modifiedComplex numbere63b2361aa8a
| Field | From #1702 | To #2259 |
|---|
| note | The structure `Complex` is defined with two real fields `re` and `im`. | Verified: `Complex` structure with `re` and `im` real fields. |
modifiedReal and imaginary parts8a2c265b87b9
| Field | From #1702 | To #2259 |
|---|
| note | Real/imaginary parts are the structure projections `Complex.re` and `Complex.im`. | Verified: structure projections `Complex.re` and `Complex.im`. |
modifiedComplex plane (Argand diagram)b1bb707a94fe
| Field | From #1702 | To #2259 |
|---|
| note | Mathlib has the bijection `Complex.equivRealProd : ℂ ≃ ℝ × ℝ` but no named 'complex plane' definition. | Verified: `Complex.equivRealProd : ℂ ≃ ℝ × ℝ` realises the Argand identification but no named 'complex plane' object. |
modifiedPurely imaginary number520de96e0c83
| Field | From #1702 | To #2259 |
|---|
| note | No dedicated 'purely imaginary' predicate; expressed via `z.re = 0`. | No dedicated 'purely imaginary' predicate; expressed inline via `z.re = 0`. |
modifiedAddition of complex numbers06303230d81d
| Field | From #1702 | To #2259 |
|---|
| note | Addition is defined componentwise via the `Add ℂ` instance at line 164 of `Basic.lean`. | Verified: componentwise addition is provided by the `Add ℂ` instance. |
modifiedParallelogram rule for additionbe0b50134bb4
| Field | From #1702 | To #2259 |
|---|
| note | The geometric parallelogram visualization for complex addition is not stated as a lemma. | The geometric parallelogram visualization is not stated as a lemma. |
modifiedMultiplication of complex numbers173b398002aa
| Field | From #1702 | To #2259 |
|---|
| note | Multiplication is defined via the `Mul ℂ` instance at line 206 of `Basic.lean`. | Verified: multiplication via the `Mul ℂ` instance gives the (ac-bd, ad+bc) formula. |
modifiedSample productbd39dd3a680b
| Field | From #1702 | To #2259 |
|---|
| note | Illustrative numeric example, no corresponding Mathlib lemma. | Illustrative numeric example with no corresponding Mathlib lemma. |
addedi squared equals -10b6594ac3e80
modifiedComplex numbers form a fielda8ad76c01160
| Field | From #1702 | To #2259 |
|---|
| note | The `Field ℂ` instance is established at line 678 of `Basic.lean`. | Verified: `Field ℂ` instance is registered. |
modifiedComplex conjugateb3b2d7b2d9d1
| Field | From #1702 | To #2259 |
|---|
| mathlib.decl | Complex.conj | starRingEnd |
| mathlib.module | Mathlib.Data.Complex.Basic | Mathlib.Algebra.Star.Basic |
| note | Conjugation is the `star` operation on ℂ, available as `conj` in the `ComplexConjugate` scope. | Conjugation on ℂ is `starRingEnd ℂ` (notation `conj` in the `ComplexConjugate` scope); a bare `Complex.conj` decl does not exist. |
modifiedConjugation is an involutionb77546f80947
| Field | From #1702 | To #2259 |
|---|
| note | Aliased as `Complex.conj_conj := starRingEnd_self_apply`. | Verified: `Complex.conj_conj` (alias of `starRingEnd_self_apply`) gives `conj (conj x) = x`. |
modifiedReal iff equals conjugate5528ea52d934
| Field | From #1702 | To #2259 |
|---|
| note | Stated at line 467 of `Basic.lean` as `conj z = z ↔ ∃ r : ℝ, z = r`. | Verified: `conj z = z ↔ ∃ r : ℝ, z = r`. |
modifiedAbsolute value (modulus)a8f7c0ac68e2
| Field | From #1702 | To #2259 |
|---|
| note | Modulus is the norm: `‖z‖ = √(normSq z)`, via the `NormedField ℂ` instance. | Verified: modulus is the norm `‖z‖ = √(normSq z)` from the `NormedField ℂ` instance. |
modifiedModulus as distancea5f0e5bc1f01
| Field | From #1702 | To #2259 |
|---|
| note | `dist z w = ‖z - w‖` in ℂ; specialising to w = 0 gives the distance from origin. | Verified: `dist z w = ‖z - w‖` on ℂ; specialising to w = 0 recovers distance from origin. |
modifiedReciprocal of a complex numbera9a1ef3942f2
| Field | From #1702 | To #2259 |
|---|
| note | `z⁻¹ = conj z * (normSq z)⁻¹` is proved at line 648 of `Basic.lean`. | Verified: `Complex.inv_def` proves `z⁻¹ = conj z * (normSq z)⁻¹`. |
modifiedDivision of complex numbersa592ea9f5954
| Field | From #1702 | To #2259 |
|---|
| note | Division is provided by the `Field ℂ` instance, giving `w / z = w * z⁻¹`. | Verified: division is supplied by the `Field ℂ` instance via `w / z = w * z⁻¹`. |
modifiedArgument of a complex number594a5407a051
| Field | From #1702 | To #2259 |
|---|
| note | `Complex.arg : ℂ → ℝ` is defined at line 30 of `Arg.lean`. | Verified: `Complex.arg : ℂ → ℝ` is defined as the principal-value argument. |
modifiedPrincipal value of argument415cce236c49
| Field | From #1702 | To #2259 |
|---|
| note | Mathlib's `Complex.arg` is the principal value: `arg_mem_Ioc` shows `arg z ∈ Set.Ioc (-π) π`. | Verified: `arg_mem_Ioc` shows `arg z ∈ Set.Ioc (-π) π`, the principal range. |
modifiedPolar form9ec4603f157f
| Field | From #1702 | To #2259 |
|---|
| note | `‖x‖ * (cos (arg x) + sin (arg x) * I) = x` is the polar form identity. | Verified: `‖x‖ * (cos (arg x) + sin (arg x) * I) = x` is the polar form identity. |
modifiedProduct and quotient in polar form687c452cfba8
| Field | From #1702 | To #2259 |
|---|
| note | Mathlib has `arg_mul_eq_add_arg_iff` and `norm_mul`, but the combined statement of the multiplicative polar law is split across lemmas. | Verified: `arg_mul_eq_add_arg_iff` and `norm_mul` cover the pieces; no single combined polar product/quotient lemma. |
modifiedde Moivre's formula2c6b404fc4cf
| Field | From #1702 | To #2259 |
|---|
| note | `(cos θ + sin θ * I)^n` formula at line 539 of `Trigonometric.lean`. | Verified: `(cos θ + sin θ * I)^n = cos (n*θ) + sin (n*θ) * I` is de Moivre's formula. |
modifiedn-th roots of a complex numberac9b82a0765c
| Field | From #1702 | To #2259 |
|---|
| mathlib.module | Mathlib.RingTheory.RootsOfUnity.Complex | Mathlib.Algebra.Polynomial.Roots |
| note | General `Polynomial.nthRoots` exists and roots-of-unity in ℂ are formalized, but no single named lemma listing the n distinct n-th roots of an arbitrary complex number. | Verified: `Polynomial.nthRoots` (general definition) exists, but no single lemma enumerating the n distinct nth roots of an arbitrary complex number in polar form. |
modifiedFundamental theorem of algebrac6c96fe63494
| Field | From #1702 | To #2259 |
|---|
| note | `Complex.isAlgClosed : IsAlgClosed ℂ` is the formal statement of FTA. | Verified: `Complex.isAlgClosed : IsAlgClosed ℂ` instance is the FTA in Mathlib. |
modifiedC is algebraically closed52edd5e9c4ec
| Field | From #1702 | To #2259 |
|---|
| note | The `IsAlgClosed ℂ` instance is registered at line 50 of `Polynomial/Basic.lean`. | Verified: the same `IsAlgClosed ℂ` instance witnesses that ℂ is algebraically closed. |
modifiedQuadratic extension definition of C213bb459f6d5
| Field | From #1702 | To #2259 |
|---|
| note | Mathlib defines ℂ concretely as ℝ² rather than as a quadratic extension ℝ[X]/(X²+1). | Mathlib defines ℂ concretely as a pair of reals, not as the quadratic extension ℝ[X]/(X²+1). |
modifiedPolynomial ring R[X]3c99b7eeb3c7
| Field | From #1702 | To #2259 |
|---|
| note | `structure Polynomial (R : Type*) [Semiring R]` is defined at line 71 of `Polynomial/Basic.lean`. | Verified: `Polynomial R` is the standard polynomial-ring type over a semiring R. |
modifiedQuotient ring isomorphism7928e8c7cfcb
| Field | From #1702 | To #2259 |
|---|
| note | First isomorphism theorem for rings is in Mathlib, but no specific instance constructing ℂ as ℝ[X]/(X²+1). | Verified: the first isomorphism theorem for rings is formalised; no specific construction of ℂ as ℝ[X]/(X²+1) is provided. |
modifiedRing isomorphism to matrix fieldd9dd3fcbde54
| Field | From #1702 | To #2259 |
|---|
| anchors | [{"section":"Matrix representation of complex numbers","snippet":"is a ring isomorphism from the field of complex numbers to the ring of these matrices"},{"type":"math_alttext","value":"{\\displaystyle a+ib\\mapsto {\\begin{pmatrix}a&-b\\\\b&\\;\\;a\\end{pmatrix}}}"}] | — |
| note | No corresponding ring isomorphism ℂ ≃+* (matrices) is formalized. | No corresponding ring isomorphism between ℂ and the 2×2 real matrices is formalised. |
modifiedConvergence in Cf15b81a9f668
| Field | From #1702 | To #2259 |
|---|
| note | Convergence in ℂ is via the metric/normed structure; the homeomorphism with ℝ × ℝ gives the componentwise characterization but it is not stated as a single named lemma. | Verified: the homeomorphism `Complex.equivRealProdCLM` induces componentwise convergence; no single named lemma states the equivalence directly. |
modifiedC is a complete metric spacea32fa14c716c
| Field | From #1702 | To #2259 |
|---|
| note | `instance : CompleteSpace ℂ` at line 119 of `Analysis/Complex/Basic.lean`. | Verified: the `CompleteSpace ℂ` instance is registered in `Analysis/Complex/Basic.lean`. |
addedTriangle inequality on C6684e1106a18
modifiedComplex exponential12ed3d525712
| Field | From #1702 | To #2259 |
|---|
| note | `Complex.exp` is defined via Cauchy sequences at line 60 of `Exponential.lean`. | Verified: `Complex.exp : ℂ → ℂ` is the standard complex exponential. |
modifiedEuler's formula986e3d28a394
| Field | From #1702 | To #2259 |
|---|
| note | `exp (x * I) = cos x + sin x * I` at line 511 of `Trigonometric.lean`. | Verified: `Complex.exp_mul_I : exp (x * I) = cos x + sin x * I`. |
modifiedEuler's identityfb1a2f789416
| Field | From #1702 | To #2259 |
|---|
| note | `exp (π * I) = -1` at line 1209 of `Trigonometric/Basic.lean`. | Verified: `Complex.exp_pi_mul_I : exp (π * I) = -1` is Euler's identity. |
modifiedComplex logarithm8d4099f91b57
| Field | From #1702 | To #2259 |
|---|
| note | `Complex.log x : ℂ` is defined at line 30 of `Complex/Log.lean`. | Verified: `Complex.log : ℂ → ℂ` is the principal branch of the complex logarithm. |
modifiedPrincipal value of log5d04373797bd
| Field | From #1702 | To #2259 |
|---|
| note | Mathlib's `Complex.log` is the principal branch: `log_im x = x.arg` lies in (-π, π]. | Verified: `Complex.log_im` shows `(log z).im = z.arg`, confirming the principal branch. |
modifiedComplex exponentiationdc4120dfc953
| Field | From #1702 | To #2259 |
|---|
| note | `Complex.cpow x y = exp (log x * y)` at line 25 of `Pow/Complex.lean`. | Verified: `Complex.cpow x y = exp (log x * y)` is the standard complex power. |
modifiedFailure of power identity7dd9cfbca228
| Field | From #1702 | To #2259 |
|---|
| note | No lemma in Mathlib explicitly exhibits the failure of `(zw)^c = z^c w^c` for complex exponents. | No lemma in Mathlib explicitly exhibits the failure of `(zw)^c = z^c · w^c` for complex exponents. |
modifiedComplex trigonometric and hyperbolic functions0a5906f9063b
| Field | From #1702 | To #2259 |
|---|
| note | `Complex.sin`, `cos`, `tan`, `sinh`, `cosh`, `tanh` are all defined via `exp` in `Trigonometric.lean`. | Verified: `Complex.sin`, `Complex.cos`, `Complex.tan`, `Complex.sinh`, `Complex.cosh`, `Complex.tanh` are all defined via `Complex.exp`. |
modifiedHolomorphic function3ad8243baa7f
| Field | From #1702 | To #2259 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.FDeriv.Basic | Mathlib.Analysis.Calculus.FDeriv.Defs |
| note | Holomorphic means `DifferentiableAt ℂ f x`; no dedicated `Holomorphic` predicate, but the concept is captured. | Verified: holomorphic is `DifferentiableAt ℂ f x`; no separate `Holomorphic` predicate. |
modifiedReal-differentiable but not complex-differentiablecc80093d4092
| Field | From #1702 | To #2259 |
|---|
| note | The explicit example (e.g. conjugation) is not formalized as a lemma. | The explicit example (e.g. complex conjugation) is not isolated as a Mathlib lemma. |
modifiedCauchy–Riemann characterization44e1f1a056c4
| Field | From #1702 | To #2259 |
|---|
| mathlib.decl | DifferentiableAt.hasDerivAt_of_isLinearMap_of_cauchyRiemann | differentiableAt_complex_iff_differentiableAt_real |
| note | The `CauchyRiemann` section in `Analysis/Complex/Conformal.lean` proves the equivalence. | Verified via semantic search: this lemma states complex-differentiability ↔ real-differentiability + the Cauchy–Riemann identity `D f (i) = i · D f (1)`. |
modifiedIdentity theorem006a475b50af
| Field | From #1702 | To #2259 |
|---|
| note | The identity theorem for analytic functions on connected open sets. | Verified: identity theorem for analytic functions on preconnected open sets. |
modifiedMeromorphic function981843ce3c0e
| Field | From #1702 | To #2259 |
|---|
| note | `MeromorphicAt f x` is defined at line 36 of `Meromorphic/Basic.lean`. | Verified: `MeromorphicAt f x` predicate is defined in `Meromorphic/Basic.lean`. |
modifiedShape of a triangle99669362201d
| Field | From #1702 | To #2259 |
|---|
| note | The complex-arithmetic 'shape' invariant of a triangle is not defined in Mathlib. | The complex-arithmetic shape invariant S(u,v,w) is not defined in Mathlib. |
modifiedMarden's theorem926a5cc97378
| Field | From #1702 | To #2259 |
|---|
| note | Marden's theorem is not formalized (only the related Gauss–Lucas theorem appears in `Polynomial/GaussLucas.lean`). | Marden's theorem is not formalised (only the related Gauss–Lucas theorem is). |
modifiedAlgebraic numbers18cc5e0f958b
| Field | From #1702 | To #2259 |
|---|
| note | `IsAlgebraic R x` at line 45 of `Algebraic/Defs.lean`; algebraic numbers are elements with `IsAlgebraic ℚ x` (in ℂ). | Verified: `IsAlgebraic R x` predicate; algebraic numbers are `IsAlgebraic ℚ x` for `x : ℂ`. |
modifiedGaussian integers23877d40d4be
| Field | From #1702 | To #2259 |
|---|
| note | `GaussianInt := Zsqrtd (-1)` at line 51 of `GaussianInt.lean`. | Verified: `GaussianInt := Zsqrtd (-1)` defines ℤ[i]. |
addedRiemann zeta functionf34ef91aab12
modifiedExistence of complex eigenvalues4ad74a3e9171
| Field | From #1702 | To #2259 |
|---|
| note | Existence of an eigenvalue over an algebraically closed field at line 63 (applies to ℂ since `IsAlgClosed ℂ`). | Verified: existence of an eigenvalue over an algebraically closed field; specialises to ℂ. |
addedHermitian matrixb3a67d76a9ce
addedUnitary matrix9ff1316cc46f
modifiedAlgebraic characterization of Cfca0bee69d50
| Field | From #1702 | To #2259 |
|---|
| note | The characterization 'characteristic 0, alg. closed, transcendence degree 𝔠 ⇒ iso ℂ' is not in Mathlib. | The characterization 'characteristic 0, algebraically closed, transcendence degree 𝔠 over ℚ ⇒ ≅ ℂ' is not in Mathlib. |
modifiedTopological field characterization of C7c936f8b2419
| Field | From #1702 | To #2259 |
|---|
| note | No theorem characterizing ℝ and ℂ as the only connected locally compact fields is formalized. | No theorem characterising ℝ and ℂ as the only connected locally compact topological fields is formalised. |
modifiedCayley–Dickson construction24403da9d092
| Field | From #1702 | To #2259 |
|---|
| note | The Cayley–Dickson construction is not formalized in Mathlib. | The Cayley–Dickson construction is not formalised in Mathlib. |
addedQuaternions146ecf0f97a0
modifiedHurwitz's theorem on normed division algebras0b24c54f864a
| Field | From #1702 | To #2259 |
|---|
| note | Hurwitz's theorem on normed division algebras over ℝ is not formalized. | Hurwitz's theorem on normed division algebras over ℝ is not formalised. |
modifiedOstrowski's theorem4dffb725acda
| Field | From #1702 | To #2259 |
|---|
| note | Ostrowski's theorem classifying absolute values on ℚ is formalized in `NumberTheory/Ostrowski.lean`. | Verified: Ostrowski's classification of absolute values on ℚ. |
addedp-adic numbers605a3984454a
modifiedSplit-complex numbers25b890c4711b
| Field | From #1702 | To #2259 |
|---|
| note | Split-complex numbers are not defined in Mathlib (no `SplitComplex` type). | Split-complex numbers (`ℝ[X]/(X² − 1)`) are not formalised in Mathlib. |